VeriFast: Imperative programs as proofs

Bart Jacobs, Jan Smans, Frank Piessens
[Google Scholar] [DBLP] [Citeseer]
Read: 29 January 2020

VSTTE workshop on Tools and Experiments
2010
Topic(s): tools verification
Note(s): permission logic, separation logic, fractional permissions, permission accounting, VeriFast verifier, ghost code, SMT solver, auto-active verification
Papers: reynolds:lics:2002

VeriFast is a symbolic evaluator based on Separation Logic (wikipedia) for verifying C and Java code. Specifications can use inductive datatypes, primitive recursive functions and abstract predicates. As the name suggests, a key feature is performance though the abstract also mentions predictability.

Proof in VeriFast relies on symbolic evaluation (using an SMT solver) but can be assisted by lemmas that are written as imperative functions. I think the essence of this is that if you can prove correctness of a terminating lemma function with contract “requires P; ensures Q;”, then “P —∗ Q”. (Where “—∗” (pronounced “magic wand”) is “separating implication” from separation logic.) These lemma functions are allowed to be recursive so it is possible to write inductive proofs.

VeriFast verifier

  • VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
  • Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]