Incremental Symbolic Execution
Background
In symbolic execution—in contrast to real runtime execution—a program is executed with symbolic values, e.g., n instead of 22, which are constrained by information that the symbolic execution engine gains during the execution. For instance, from an if-condition such as 0 < n, it can be concluded that 0 < n holds in the if-branch and 0 >= n holds in the else-branch. A single symbolic execution thus summarizes an unbounded number of real executions.
Symbolic execution has been applied in various fields such as testing and automated software verification. In the latter case, a program is symbolically executed in order to show that the code meets its specifications.
Among other tools, our group develops a symbolic-execution-based verifier called Silicon. We plan to release Silicon together with a basic IDE, e.g., an Eclipse plug-in. For the IDE integration, it is important that the verifier is responsive, i.e., that it quickly reacts to small changes to the program, e.g., by putting a squiggly line below a failing assertion. This expectation is comparable to the expectations we have about IDE-integrated compilers, which often use incremental compilation in order to minimize the amount of work that needs to be re-done after a piece of code has been changed.
Goals
The goal of this Bachelor's thesis is to investigate the potential of incremental symbolic execution, i.e., to identify and implement ways of re-executing as little as possible after code has been changed. A starting point would be to only re-execute methods that have been changed, or depend on methods whose specifications have changed.
However, we aim for determining more precisely which parts of the program need to be re-verified. For instance, we might reuse cached symbolic states from previous runs if we can guarantee that they are not affected by the changes. This would allow the tool to "jump" to specific program points from which to continue the symbolic execution. Another idea would be to minimize the amount of work that needs to go into re-verifying the callers of a method whose specification changed; e.g., by checking if the new postcondition is stronger than the old one.
Opportunities
- Gain experience with symbolic execution, an interesting concept applicable in different problem domains
- Make a significant contribution towards making our verification tools more user-friendly
- Work with Scala, a modern programming language with an advanced type-system that combines object-oriented and functional concepts
Contact
Malte Schwerhoff or Valentin Wüstholz