Large 00010

The Spec# Programming System - Part 1

Prof. Peter Müller (ETHZ, Switzerland)

Recorded 17 September 2012 in Lausanne, Vaud, Switzerland

Event: ntass 2012 - Nano-Tera/Artist Summer School 2012


Spec# is a programming system, which consists of the Spec# programming language, a verification methodology, and a static verifier. The language extends C# with non-null types, method contracts, and object invariants. The verification methodology allows one to reason about complex heap data structures in the presence of aliasing and call-backs. The static verifier is based on the Boogie verification engine and the automatic theorem prover Z3. This lecture will give an introduction to the Spec# system with an emphasis on the verification methodology.

Watched 543 times.