A Bit of Butter (What Could Be Better Than Sliced Bread?): The
Spec# Programming System
Michael Barnett
Microsoft
Monday, October 18, 2:00PM
Burchard 124
Computer Science Department
Stevens Institute of Technology
Abstract
Spec# is the latest in a long line of work on programming languages
and systems aimed at improving the development of correct
software. The Spec# programming system consists of the object-oriented
Spec# programming language, the Spec# compiler, and the Boogie static
program verifier. The language includes constructs for writing
specifications that capture programmer intentions about how methods
and data are to be used, the compiler emits run-time checks to enforce
these specifications, and the verifier can check the consistency
between a program and its specifications. The Spec# programming system
is currently under development at Microsoft Research.
The audience is expected to have studied in advance
http://users.crocker.com/~slinberg/poems/milne/kingsbreakfast.html.
Joint work with Rob DeLine, Manuel Fahndrich, Rustan Leino, Wolfram
Schulte, Herman Venter, Peter Muller, and Dave Naumann