wiki:WikiStart
Last modified 3 years ago Last modified on 03/03/12 19:31:28

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

Formalization and Proofs

Prototype Implementation

Further resources