TL;DR
Featherweight VeriFast provides a formal, rigorous, and machine-verified core model of the VeriFast program verification tool, enhancing understanding and trust in its soundness for verifying safety and correctness properties.
Contribution
This paper offers the first formal, executable, and machine-checked definition and proof of soundness for a core subset of VeriFast's verification approach.
Findings
Formal definition of VeriFast core subset
Machine-checked soundness proof in Coq
Accessible yet rigorous exposition
Abstract
VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFast's operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
