wiki:WikiStart

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