Programmanalysis: Theory and Applications
- The Course will take pace in Sarntal from 22th of September until 5th of October 2013
- Talks can be given in German or English
- The deadline for applications is the 12th of May
Program analysis is the art of computing information about the structure and behaviour of programs. There are all kins of analyzers. Some compute generic information, like e.g. a list of all variables, the class hierarchy, the call graph, or the architecture of a system. Others search more specifically for features like
- Dead code. This is code that can never be executed, and so can be safely removed from the program. Compilers routinedly conduct some analysis to remove dead code.
- Violations of programming guidelines.
- Bug patterns. These are suspect program constructs which point to the presence of a bug.
- Clones. Clones are identical or similar pieces of code, which are often a result of copying and pasting as an act of ad-hoc reuse by programmers. Software errors in cloned pieces of code are particularly dangerous.
Finally, some analyzers even inspect exhaustively the executions of a model of the program, and detect executions producing undesired effects.
Analyzers are deployed at all levels of the software design process. Compilers use them to optimize the object code, antivirus-software use them to detect malicious software patterns, and quality assurance systems use them to enforce guidelines and detect bugs.
Here are some links to the web pages of important state-of-the-art analyzers:
- LLVM. A compiler infrastructure comprising several analyzers that, for instance, evaluate dynamic paths through a program in an effort to find bugs, or instrument code with run-time checks to detect memory safety errors. Winner of the 2012 ACM Software System Award.
- Astree. A program analyzer aiming at proving the absence of Run Time Errors in C programs.
- Coverity's quality advisor. A program analyzer aimed at finding errors like memory corruptions, null pointer dereferences, or performance inefficiencies.
In the course we will examine several analyzers which well documented, particularly easy to install and work with, and accessible to students in their first or second year. Course articipants will work in groups of two or more. Each group will be assigned a tool. Under the guidance of a supervisor, the team will present the main ideas behind the tool, and will demonstrate it on interesting examples.
Here is an initial list of the tools that will be considered.
Spin is a popular open-source software verification tool. The tool can be used for the formal verification of multi-threaded software applications, including shared memory and buffered message passing. The tool was developed at Bell Labs in the Unix group of the Computing Sciences Research Center. The tool supports a high level language to specify systems descriptions called PROMELA, but also offers support for embedded C code. Spin checks the logical consistency of a specification and reports on deadlocks, race conditions, different types of incompleteness, and unwarranted assumptions about the relative speeds of processes.
Soot is an academic Java Analyzing and Optimizing framework, developed by Patrick Lam et al. at McGill University in Montreal. It reads Java classes and offers multiple interesting intermediate representations of this bytecode. On top of that, Soot offers a Java framework to specify and run dataflow analyses through worklist based fixpoint iteration on dataflow equations. To make using Soot even more convenient, the programmer can access the results of already provided standard analyses like intervals or available expressions.
FindBugs, created at the University of Maryland, is a tool to analyze Java-bytecode for bug patterns. These bug patterns emerged from different sources, e.g. difficult language constructs, common careless mistakes or even commonly missinterpreted API methods. FindBugs analyzes the software and yields a list of warnings with potential mistakes, which correspond to the bug patterns. These remain to be processed by the programmer, improving his or her code:
ConQAT was originally developed as a tool for aggregating continually captured analysis data. Such tools are also called dashboards, cockpits or control panels. However, ConQAT also comprises several standalone analyses, which can be executed without any other tool. In the context of the Ferienakademie, we want to focus primarily on its clone analysis. Software-clones are repeatedly occuring code fragments. They complicate the maintainance of software, as fixes potentially have to be applied at several locations and code is unnecessarily bloated. ConQAT is able to locate these copied fragments and help the developer to maintain these code parts consistently or to replace them.
- Modern Jass:
Modern Jass is a tool for carry the idea of "Design by Contract" to Java. Therefore, Modern Jass relies on Java-Annotationen, in order to specify the behaviour of methods and other code fragments. This specification is carried out with the help of special annotations, e.g. @pre for specifying preconditions. These "contracts" are then evaluated via a plugin in the IDE. This enables the developer to analyse, whether a method's behaviour matches the expectations, or whether they are used as intended, quite early in the development phase: