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.
|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 Sep 2011 → 10 Sep 2011
|Seminar||8th LASER Summer School on Software Engineering|
|Period||04/09/2011 → 10/09/2011|