VeriFast: A powerful, sound, predictable, fast verifier for C and Java

Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 09 February 2020

NASA Formal Methods Symposium
Springer
Pages 41-55
2011
Topic(s): tools verification
Note(s): permission logic, separation logic, fractional permissions, permission accounting, VeriFast verifier, ghost code, SMT solver, auto-active verification
Papers: bornat:popl:2005, jacobs:vstte:2010, philippaerts:scp:2014

VeriFast is an auto-active verification tool for C and Java based on separation logic and SMT solvers. This paper is a nice overview of the state of the project in 2011 when they had

a symbolic execution based checker with a nice UI
support for both C and Java
support for permission accounting based on fractional permissions and an encoding of counting permissions
support for writing (recursive) lemma functions to prove inductive properties
and they were starting on some industrial case studies

VeriFast verifier

Leveraging Rust types for modular specification and verification [astrauskas:oopsla:2019]
Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
The Boogie verification debugger [legoues:sefm:2011]
Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]
Implicit dynamic frames: Combining dynamic frames and separation logic [smans:ecoop:2009]
Local reasoning about while-loops [tuerk:vstte:2010]

VeriFast: A powerful, sound, predictable, fast verifier for C and Java

Notes related to VeriFast: A powerful, sound, predictable, fast verifier for C and Java

Papers related to VeriFast: A powerful, sound, predictable, fast verifier for C and Java