Featherweight VeriFast

By Frédéric Vogels, Bart Jacobs, and Frank Piessens

Featherweight VeriFast is a formally defined program verification approach that captures a core subset of the VeriFast approach for sound modular verification of imperative programs.

An executable machine-readable definition and machine-checked soundness proof of Mechanised Featherweight VeriFast, a slight variant of Featherweight VeriFast, is given below.

The following article formally defines Featherweight VeriFast, outlines a soundness proof, and describes the mechanisation.

Featherweight VeriFast [PDF] [Slides] [Handouts]
By Frédéric Vogels, Bart Jacobs, and Frank Piessens.
In Logical Methods in Computer Science 11(3:19), 2015.

Mechanised Featherweight VeriFast

The following input files for the Coq 8.4 formal proof management system constitute a machine-readable executable definition and machine-checked soundness proof of Mechanised Featherweight VeriFast.

• Util: Some basic definitions
• The Programming Language
  • Programs: The syntax of programs
• Concrete Execution
  • Outcomes: The semantic framework in which the three executions are expressed
  • ConcreteExecution: The semantics of programs, with a small test suite
    Concrete execution is semi-executable in the sense that algorithms are defined for checking that a given sequence of demonic choices leads to a singleton outcome or to failure
• Semiconcrete Execution
  • SemiconcreteStates: Mostly lemmas about semiconcrete heaps (which are multisets of chunks)
  • SemiconcreteExecution: An intermediate execution between concrete and symbolic execution
  • ConsumeProduce: Properties of consumption and production and heap refinement
  • ConcreteExecutionFacts: Some basic facts about some concrete mutators
  • SemiconcreteExecutionFacts: Some basic facts about some semiconcrete mutators
  • Locality: Locality of semiconcrete mutators
  • Modifies: Proof that semiconcrete execution of a command modifies only its targets
  • SemiconcreteSoundness: Soundness of semiconcrete execution
• Symbolic Execution
  • SMT: A minimal SMT solver (used by SymbolicExecution)
  • SymbolicExecution: The verification algorithm, with a small test suite
    Symbolic execution is executable: Compute svalid_program rspecs preddefs rdefs c prints either ok or error message
  • SMTSoundness: Soundness of the SMT solver
  • SymbolicExecutionFacts: Some basic facts about some symbolic mutators
  • EnsemblesEx: Notations and lemmas about ensembles (sets as predicates)
  • PartialInterpretations: Partial interpretations
  • SymbolicSoundness: Soundness of symbolic execution
  • Soundness: The main soundness theorem: symbolic execution is sound with respect to concrete execution

See also: [Sources] [Contents] [Index] [PDF] [Module dependencies]

To type-check the definitions, run the test suite, and check the soundness proof, issue the following commands, with Coq 8.4 in your PATH:

coq_makefile *.v > Makefile
make

Coq will print the list of axioms used by the soundness proof. Note that all axioms are from the Coq standard library and are axioms of classical logic.