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
Pages 41-55
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

VeriFast verifier