Using Dafny, an Automatic Program Verifier

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

Using Dafny, an Automatic Program Verifier

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

Microsoft USA

Research output: Contribution to conference › Paper › Research › peer-review

4569 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 language	English
Publication date	2011
Number of pages	26
Publication status	Published - 2011
Event	8th LASER Summer School on Software Engineering: Tools for Practical Software Verification - Elba Island, Italy Duration: 4 Sept 2011 → 10 Sept 2011 http://laser.inf.ethz.ch/2011/

Seminar

Seminar	8th LASER Summer School on Software Engineering
Country/Territory	Italy
City	Elba Island
Period	04/09/2011 → 10/09/2011
Internet address	http://laser.inf.ethz.ch/2011/

Access to Document

DafnyLectureNotes

OpenUrl availability

Full text

Cite this

@conference{6296a92733c54eb9abb808dc77312beb,

title = "Using Dafny, an Automatic Program Verifier",

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.",

author = "Herbert, {Luke Thomas} and Leino, {K. Rustan M.} and {Carvalho Quaresma}, {Jose Nuno}",

year = "2011",

language = "English",

note = "8th LASER Summer School on Software Engineering : Tools for Practical Software Verification ; Conference date: 04-09-2011 Through 10-09-2011",

url = "http://laser.inf.ethz.ch/2011/",

}

TY - CONF

T1 - Using Dafny, an Automatic Program Verifier

AU - Herbert, Luke Thomas

AU - Leino, K. Rustan M.

AU - Carvalho Quaresma, Jose Nuno

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

M3 - Paper

T2 - 8th LASER Summer School on Software Engineering

Y2 - 4 September 2011 through 10 September 2011

ER -

Using Dafny, an Automatic Program Verifier

Abstract

Seminar

Access to Document

OpenUrl availability

Fingerprint

Cite this