One of the challenges in automatic program verification tools such as the VCC verifier and the VeriFast verifier is the amount of annotation required to write the specification and guide the verification tool to construct a proof.
The VeriFast tool’s initial goal was to provide sound, fast verification for C and Java. This paper describes three extensions to reduce the amount of annotation required. These extensions are implemented outside the small core and therefore any annotations added cannot cause VeriFast to produce unsound results.
-
In VeriFast, one often “opens” a predicate at the start of a function to expand the predicate’s definition and “closes” a predicate at the end of a function to trigger proof that the predicate holds, The first auto-annotations technique is to automatically open/close any predicates mentioned in the requires/assumes clauses provided the predicates are not recursive. The basis for this is a directed graph between predicates that mention each other where edges are labelled with side-conditions.
-
In VeriFast, one also explicitly applies lemmas. The second auto-annotation aggressively applies lemmas as soon as possible (i.e., as soon as they can be triggered) to make all consequences available to the prover unless doing so could lead to an exponential explosion or would remove facts from the symbolic state.
-
Finally, they perform a shape analysis, which further drives open/close, lemma application and also loop invariant generation.
The overall effect of these three inference steps is a dramatic reduction in the amount of annotation required. Across eight functions totalling 113 lines of code, the amount of annotation required drops from 205 lines of annotation to just 8 lines of annotation.
Notes related to Annotation inference for separation logic based verifiers
Papers related to Annotation inference for separation logic based verifiers
- Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]