Dafny to Boogie Translation

Apr 14, 2013 at 12:45 PM
Hi there,

i want to check about "how Dafny code is translated into boogie" and "how BVD (Boogie verification debugger)" can help us to verify the Dafny program.

i am looking for some references (i.e. reference material)

thanks in advance !
-asif
Coordinator
Apr 15, 2013 at 10:07 PM
The best source for "how Dafny code is translated into Boogie" are my Marktoberdorf 2008 summer school lecture notes. They describe the translation of the basic features in detail. For features that were added since 2008, the best overview is the Dafny paper from LPAR-16. You'll find these mentioned in the "Learn more" section on the Dafny page.

There are also specialized papers that describe induction, co-induction, and verified calculations, respectively. These ought to be listed on the Dafny page as well, but for now you can find some preprints of them on my papers page.

For BVD, I first recommend the BVD paper, which shows some examples of what you can do. You can find that paper here.

Rustan