Using Dafny, an Automatic Program Verier

  • Luke Herbert ,
  • Rustan Leino ,
  • Jose Quaresma

in Tools for Practical Software Verification

2012 | Tools for Practical Software Verification edition

View Publication

These lecture notes present Dafny, an automated program verification system that is based on the concept of dynamic frames and is capable of producing .NET executables. These notes overview the basic design, Dafny’s history, and summarizes the environment configuration. The key language constructs, and various system limits, are illustrated through the development of a simple Dafny program. Further examples, linked to online demonstrations, illustrate Dafny’s approach to loop in-variants, termination, data abstraction, and heap-related specifications.

Publication Downloads


January 2, 2017

Dafny is a verification-aware programming language.