Annotation inference for VeriFast

VeriFast is an approach for modularly verifying correctness properties of single-threaded and multithreaded imperative and object-oriented programs. In the approach, the programmer inserts into the program's source code annotations that define a module's specification (in the form of procedure preconditions and postconditions expressed in separation logic) and annotations that prove the module implementation's compliance with its specification (in the form of separation logic predicate definitions, loop invariants, lemma procedures, and proof hints). The programmer then invokes a verification tool that takes the annotated source code as input and, without further user interaction and typically in a matter of seconds, either reports that no errors were found, or indicates a procedure whose proof failed, together with a symbolic execution trace leading to the failure. If no errors were found, this implies that none of the program's executions fail or violate the specified properties. The VeriFast approach is a leading approach for modular program verification, thanks to the fact that it combines proof power with good and predictable verification performance.

In this project, we propose to perform research on techniques that reduce the annotation effort required to apply the VeriFast approach, by automatically generating as many annotations as possible. Our goal is to integrate ideas from the automatic program analysis literature to obtain the best of the two worlds.