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