Software and Computational Systems Lab

Program testing is an established technique in modern software development, but it is, in most cases, not able to cover all potential program paths. In practice, even incomplete coverage goals like branch coverage are not always fulfilled by hand-written tests. Thus, bugs may go unnoticed. In contrast to this, symbolic execution is a program analysis technique that is able to exhaustively analyze a program by executing a program with symbolic inputs instead of concrete ones. During this symbolic execution, constraints on the symbolic inputs are recorded. These constraints show relations between inputs and can be used to create a test suite that fully meets a given coverage goal.

Theses in this topic are concerned with implementing heuristics or improvements to an existing symbolic execution engine in CPAchecker (implemented in Java).

Experimental evaluation of the effect of compiler optimizations and automatic code transformations of GCC or LLVM on code analyses like formal verification or automated testing. Topic may be related to good, bad, ugly interpolants.

There are many different ways to find out whether a program is buggy, for example testing or formal verification. Once we know that a program is buggy, i.e., that it shows some faulty behavior, a developer has to manually debug the program to find the cause of the problem and fix it - this is a difficult and long-taking process. The aim of this thesis is to help programmers with debugging by implementing one such technique to automatically find potential causes for faulty behavior and present the found causes.

An SMT formula is a boolean formula that includes numbers and common arithmetic operations. Since formal verification techniques often use SMT formulas to represent programs and models , the speed of solving SMT formulas is a very important aspect of formal verification. Studies show that SMT formulas that are created by model checkers or symbolic execution often have a specific structure: The relation between program variables (e.g., "x == y + z") is dependent on program constraints over these variables that only contain a single variable each, e.g., x > 0, y > 0, and z > 10. This example would be represented as the SMT formula x == y + z ∧ x > 0 ∧ y > 0 ∧ z > 10.

The satisfiability of SMT formulas with this specific structure can be computed through the following decision procedure:
1. For each program variable in the formula, compute the interval(s) of possible values for this variable for which the constraints of this variable are satisfied, and
2. Check whether the relations between program variables can be satisfied with the computed intervals.

The goal of this topic is to implement this procedure and to make it available as a Java library. Work on this in the symbolic execution engine Klee has shown great potential, leading to speedups of up to 55x compared to the use of existing complete SMT solvers.