The VeriFast program verifier

Abstract

This note describes a separation-logic-based approach for the spec-ification and verification of safety properties of pointer-manipulating imperative programs. We describe the approach for the C language. The safety properties to be verified are specified as annotations in the source code, in the form of function preconditions and post-conditions expressed as separation logic assertions. To enable rich specifications, the user may include additional annotations that de-fine inductive datatypes, primitive recursive pure functions over these datatypes, and abstract predicates (i.e. named, parameterized assertions). A restricted form of existential quantification is sup-ported in assertions in the form of pattern matching. Verification is based on forward symbolic execution, where memory is represented as a separate conjunction of points-to as-sertions and abstract predicate assertions, and data values are rep-