Creating an Advanced Debugger for Symbolic Execution
Program verifiers check that a program satisfies its specification. So, if a verifier reports "no errors found", the program is definitely correct. However, if verification fails, the situation is less clear. It could be that the implementation is incorrect. Or maybe there is something wrong with the specifications?
Verification debugging is the process of understanding the reason why a given program does not verify. One of the key limitations of verification debuggers comes from the fact that the tools are static. A traditional program debugger has exact information about the program’s runtime. In contrast, a static program verifier has to reason about all possible behaviors at once. One useful technique for reasoning about multiple program behaviors at once is via symbolic state — for example, we can draw the configuration of the heap before and after a method call in order to understand the overall effect of this operation.
In this project, we will create a new verification debugger that benefits from the rich spectrum of information available in Silicon, our state-of-the-art symbolic execution verifier. In Silicon, the symbolic program states are explicitly present at intermediate symbolic execution steps.
The screenshot shows the current prototype implementation of the symbolic execution debugger. The left column displays a Viper program annotated with state markers; the middle column shows the old (previous) symbolic state of the program; the right column shows the new (current) symbolic state. This allows the programmer to see the effect of the operations between two states.
The project is set in the context of ViperIDE, a modular infrastructure for integrating verification tools developed in our group. Detailed information about ViperIDE can be found here: Download Advanced Features for an Integrated Verification Environment.
The main research challenge is to find a useful way of visualizing ambiguous symbolic state in a way that benefits the programmer. The main engineering challenge is to create a practical system based on several existing components.
These are the main goals of the project:
- Extend the logger for collecting symbolic execution information on a fine-grained level.
- Extend existing IDE protocols for making symbolic execution information available to the client.
- Design and implement the visual verification debugger (based on an existing prototype).
- Find a practical way to visualize the symbolic state for different verification scenarios. In particular, support dynamically bounded data structures, such as arrays.