DVerify

DVerify is a tool for automatically verifying  Dminor programs using the  Boogie generic verification condition generator backend. The soundness of the translation algorithm from Dminor to Boogie has been proved formally using  Coq.

Research

• Michael Backes,  Cătălin Hriţcu, and Thorsten Tarrach.  Automatically Verifying Typing Constraints for a Data Processing Language. In  First International Conference on Certified Programs and Proofs (CPP 2011), 296-313, Springer, December 2011. ( slides PDF)
  •  Preliminary version presented at the  BOOGIE 2011 workshop, 1 August 2011. (slides  PDF  Powerpoint)

• Thorsten Tarrach,  Automatically Verifying "M" Modeling Language Constraints, Master's Thesis, Information Security and Cryptography Group, Saarland University, September 2010.
  •  Slides from Master's Seminar talk (introductory talk).
  •  Slides from thesis defense talk.

•  Gavin M. Bierman,  Andrew D. Gordon,  Cătălin Hriţcu, David Langworthy.  Semantic Subtyping with an SMT Solver, In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), September 2010.
  • More information can be found on  the Dminor project website at Microsoft Research.

Formalization and Proofs

•  Coq formalization and proofs by Thorsten Tarrach.  Creative Commons - Attribution 3.0 Unported License.
  • Built on top of the  Coq formalization of Dminor by  Cătălin Hriţcu.  Creative Commons - Attribution 3.0 Unported License.

Prototype Implementation

•  DVerify 1.0 by Thorsten Tarrach. Source and Binaries.  Apache 2.0 License.

Further resources

•  The Dminor type-checker by Microsoft Research Cambdridge
•  The code name "M" modeling language as described at  Microsoft PDC 2009 ( apparently discontinued)
•  The Boogie verification condition generator
•  The Z3 SMT-solver
•  The Coq proof assistant