Profiling and Debugging Automated Program Verification
General Background
In deductive verification, our goal is to mathematically prove that a program fulfills a formal specification (consisting, for example, of a pre- and a postcondition). Tools like Viper automate this process: Given a program, a specification, and some annotations to guide the proof search, they automatically either construct a proof or point out a part of the program that may have an error.
One way of doing this is symbolic execution, where the prover essentially walks through all the paths in the program, computes which conditions have to be checked for each statement on the path (e.g., for an array access, that the index is in bounds), and then asks an SMT solver like Z3 to automatically prove that these conditions hold on the current path. However, since these queries are in general undecidable, this process does not always succeed, and the SMT solver may take very long to respond or not terminate at all.
This is, in a sense, the worst case for automated verification, since the user is left without any feedback and does not even know which part of the program poses problems for the verifier. As a result, even existing debugging tools that can be used when the verifier terminates but reports a verification error do no apply in this scenario.
Project Background
In this project, we want to address this problem by creating a profiling and debugging technique that does not rely on the verifier's termination. The central idea is, in a first step, to collect all proof obligations our verification tools would normally give to the SMT solver, without actually asking the SMT solver to check them. Once we have these queries, we can give a first overview of the verification problem, and show users e.g. how many paths through the program are actually being checked, and which queries have to be proved at which point. Now, we can give individual queries to the SMT solver with a timeout, in order to identify which queries take long to verify and are therefore worth investigating in detail.
Once an individual problematic query has been identified, there are several options for helping users to debug the problem, e.g., by excluding some assumptions from the proof, letting users add custom proof obligations, displaying statistics about the unsuccessful proof search, or integrating existing tools for SMT debugging.
Goals
- Design a technique for extracting proof queries from a symbolic execution based verifier in such a way that dependencies between queries are recorded and queries can be displayed to users.
- Implement this technique for Viper's existing symbolic execution based verifier.
- Enable users to automatically identify problematic queries.
- Design and implement different ways for users to debug problematic queries, and/or integrate existing SMT debugging tools.
- Potentially integrate the entire technique with Viper's existing VSCode based IDE.
Useful Prerequisites
Experience with verification (e.g., from the Program Verification course at our department) would be very advantageous; for students aiming for more focus on IDE integration, experience with VSCode would be great.