A Tutorial on Using Dafny to Construct Verified Software

Paqui Lucio

This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.

In Alicia Villanueva: Proceedings XVI Jornadas sobre Programación y Lenguajes (PROLE 2016), Salamanca, Spain, 14-16th September 2016, Electronic Proceedings in Theoretical Computer Science 237, pp. 1–19.
Published: 11th January 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.237.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org