Using Dafny, an Automatic Program Verifier

Luke Thomas Herbert, K. Rustan M. Leino, Jose Nuno Carvalho Quaresma

    Research output: Contribution to conferencePaperResearchpeer-review

    3410 Downloads (Pure)

    Abstract

    These lecture notes present Dafny, an automated program verication 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 conguration. 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 specications.
    Original languageEnglish
    Publication date2011
    Number of pages26
    Publication statusPublished - 2011
    Event8th LASER Summer School on Software Engineering: Tools for Practical Software Verification - Elba Island, Italy
    Duration: 4 Sep 201110 Sep 2011
    http://laser.inf.ethz.ch/2011/

    Seminar

    Seminar8th LASER Summer School on Software Engineering
    Country/TerritoryItaly
    CityElba Island
    Period04/09/201110/09/2011
    Internet address

    Fingerprint

    Dive into the research topics of 'Using Dafny, an Automatic Program Verifier'. Together they form a unique fingerprint.

    Cite this