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.
- 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)
- Thorsten Tarrach, Automatically Verifying "M" Modeling Language Constraints, Master's Thesis, Information Security and Cryptography Group, Saarland University, September 2010.
- 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.