Certified Program Verification with Coq

The general aim of this project is to use the idea of developing program verification tools with proofs of soundness in Coq to make Foundational Proof-Carrying Code practical enough to use at all levels of computer systems.

  • ICFP paper: Modular Development of Certified Program Verifiers with a Proof Assistant
  • Online documentation
  • To download the source distribution, follow the instructions in the documentation for checking out the CVS repository.


    Author: Adam Chlipala

    Project summary page

    SourceForge Logo