- The VeriFast program verifier
By Bart Jacobs and Frank Piessens
Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, August 2008
[PDF] - The VeriFast Program Verifier: A Tutorial
[PDF] [illegal_access.c] - Verification of Imperative Programs: The VeriFast Approach -- A Draft Course Text
By Bart Jacobs, Jan Smans, and Frank Piessens
Technical Report CW-578, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, March 2010
Presents a formalization and soundness proof of a core subset of the VeriFast approach
[PDF] - Verifying the Composite Pattern using Separation Logic
By Bart Jacobs, Jan Smans, and Frank Piessens
SAVCBS 2008 Composite pattern challenge track, October 2008
[PDF] - Dynamic Owicki-Gries reasoning using ghost fields and fractional permissions
By Bart Jacobs and Frank Piessens
Technical Report CW-549, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, June 2009
[PDF] - Verification of data-race-freedom of a Java chat server with VeriFast
By Cedric Cuypers, Bart Jacobs, and Frank Piessens
Technical Report CW-550, Department of Computer Science, Katholieke Universiteit Leuven, Belgium, June 2009
[PDF] - VeriFast: Imperative Programs as Proofs
By Bart Jacobs, Jan Smans, and Frank Piessens
Presented at the VS-Tools workshop at VSTTE 2010, August 2010 (no formal proceedings)
[PDF] - A Quick Tour of the VeriFast Program Verifier
By Bart Jacobs, Jan Smans, and Frank Piessens
In Proc. APLAS 2010, tool paper track, LNCS 6461, pp. 304-311, November 2010
[PDF] - Expressive Modular Fine-Grained Concurrency Specification
By Bart Jacobs and Frank Piessens
In Proc. POPL 2011. ACM SIGPLAN Notices 46(1), pp. 271-282, January 2011
[PDF] [Slides (PDF)] [TR] [Coq proof] - Verification of unloadable modules
By Bart Jacobs, Jan Smans, and Frank Piessens
In Proc. FM 2011
[PDF] [Slides (PDF)] [TR] [Coq proof] - The VeriFast Program Verifier: A Tutorial for Java Card Developers
[PDF] (Note: for "the VeriFast tutorial", see above.) - VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
By Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens
Invited paper, in Proc. NASA Formal Methods (NFM) 2011
Describes: the basic symbolic execution approach in some formal detail; permission accounting (fractions and counting) and precise predicates; lemma function termination
[PDF] - The Belgian electronic identity card: a verification case study
By Pieter Philippaerts, Frédéric Vogels, Jan Smans, Bart Jacobs, and Frank Piessens
In Proc. International Workshop on Automated Verification of Critical Systems (AVOCS'11), Newcastle, 12-14 September 2011
[PDF] - Sound formal verification of Linux's USB BP keyboard driver
By Willem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, and Frank Piessens
In Proc. NASA Formal Methods (NFM 2012), Norfolk, Virginia, USA, 3-5 April 2012
[PDF] [More info] - Software verification with VeriFast: industrial case studies
By Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, and Frank Piessens
Science of Computer Programming 82(1), pp. 77-97, March 2014
[PDF] - VeriFast for Java: A Tutorial
By Jan Smans, Bart Jacobs, and Frank Piessens
In Dave Clarke, Tobias Wrigstad, and James Noble (Eds.), Aliasing in Object-Oriented Programming, LNCS 7850, Springer, 2013
[PDF] - Sound symbolic linking in the presence of preprocessing
By Gijs Vanspauwen and Bart Jacobs
In Proc. 11th International Conference on Software Engineering and Formal Methods (SEFM 2013), LNCS 8137, Springer, 2013
[PDF] - Solving the VerifyThis 2012 challenges with VeriFast
By Bart Jacobs, Jan Smans, and Frank Piessens
In International Journal on Software Tools for Technology Transfer, 2014
[PDF] - Verifying TSO programs
By Bart Jacobs
Technical report CW660, Department of Computer Science, KU Leuven, May 2014
[PDF] - Shared boxes: rely-guarantee reasoning in VeriFast
By Jan Smans, Dries Vanoverberghe, Dominique Devriese, Bart Jacobs, and Frank Piessens
Technical report CW662, Department of Computer Science, KU Leuven, May 2014
[PDF] - Sound, modular and compositional verification of the input/output behavior of programs
By Willem Penninckx, Bart Jacobs, and Frank Piessens
In Proc. ESOP 2015
[PDF] - Modular termination verification
By Bart Jacobs, Dragan Bosnacki, and Ruurd Kuiper
At ECOOP 2015
[PDF] [TR] - Provably live exception handling
By Bart Jacobs
At FTfJP 2015
[PDF] - Featherweight VeriFast
By Frédéric Vogels, Bart Jacobs, and Frank Piessens
In Logical Methods in Computer Science 11(3:19), 2015
[PDF] [Slides, handouts, Coq proof] - Verifying protocol implementations by augmenting existing cryptographic libraries with specifications
By Gijs Vanspauwen and Bart Jacobs
At SEFM 2015
[PDF]
Support
This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen), by the EU FP7 project SecureChange, by Microsoft Research Cambridge as part of the Verified Software Initiative, by the EU FP7 projects ADVENT and STANCE, and by Research Fund KU Leuven.
Third-party research that uses VeriFast
- Luyi Xing, Xiaorui Pan, Rui Wang, Kan Yuan, and Xiaofeng Wang. Upgrading Your Android, Elevating My Malware: Privilege Escalation Through Mobile OS Updating. In Proc. 35th IEEE Symposium on Security and Privacy (IEEE Oakland), 2014.
- Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, and George Candea. A Formally Verified NAT. In Proc. SIGCOMM, 2017.
- Andrei Damian, Cezara Dragoi, Alexandru Militaru, and Josef Widder. Communication-closed asynchonous procotols. TR hal-01991415, version 1, INRIA, 2019.