Michael Barnett, Microsoft

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

Co-sponsored by Laboratory for Secure Systems, New Jersey Institute for Trustworthy Enterprise Software, and the PORTIA project.