Authors: Bart Jacobs ; Frédéric Vogels ; Frank Piessens

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 rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq.

• 03B70 - Logic in computer science
• 68N15 - Theory of programming languages
• 68N19 - Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
• 68N30 - Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
• 68Q60 - Specification and verification (program logics, model checking, etc.)