Advertisement
Published in:
2012 | OriginalPaper | Chapter
Using Dafny, an Automatic Program Verifier
Authors : Luke Herbert, K. Rustan M. Leino, Jose Quaresma
Published in: Tools for Practical Software Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 invariants, termination, data abstraction, and heap-related specifications.