Mostly sound type system improves a foundational program verifier
Josiah Dodds
and
Andrew W. Appel
Princeton University
Welcome to the website for our CPP submission.
Current release of VST, containing all typechecker and proof automation files:
VST version 0.9
For advice on installing, see the first chapter of the
Verifiable C manual, listed
below. Release 0.9 is compatible with the CompCert trunk, revision 5335.
VST release 1.0 is expected to be compatible with CompCert release 2.0, in summer 2013.
Bleeding edge (under active development):
VST subversion repository
A brief tour of the code follows in order of how interesting we expect the files will be to a reader. All files listed here are contained in the veric directory of all above packages.
expr.v
definitions for the computational expression evaluator, as well as the typechecker, type envrionment, and environment typechecker
expr_lemmas.v
main soundness lemmas for typechecker and the proof relating the computational expression evaluation to CompCert's evaluation relation
SeparationLogic.v
specification of the separation logic