VeriFast is a verifier for C and Java programs based on separation logic developed at KU Leuven. VeriFast includes support for fractional permissions

Notes related to VeriFast verifier

Annotation burden, Auto active verification, Separation logic, Symbolic execution

Papers related to VeriFast verifier

• Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
• VeriFast: A powerful, sound, predictable, fast verifier for C and Java [jacobs:nfm:2011]
• VeriFast: Imperative programs as proofs [jacobs:vstte:2010]
• Sound formal verification of Linux's USB BP keyboard driver [penninckx:nfm:2012]
• Software verification with VeriFast: Industrial case studies [philippaerts:scp:2014]
• Local reasoning about while-loops [tuerk:vstte:2010]
• Annotation inference for separation logic based verifiers [vogels:fmoods:2011]