VeriFast: Imperative Programs as Proofs

This paper describes the VeriFast prototype program verification tool, which implements a separation-logic-based approach for the specification and verification of safety properties of pointer-manipulating imperative programs. The approach's distinctive feature is that it combines very good and predictable verification performance with powerful proofs written conveniently as part of the program. We describe the tool's support for the C language. The paper introduces the tool's various features by means of a running example of a linked list implementation. A detailed formalization of the core of the approach and a soundness proof are available on the website.status: publishe