A Bit of Butter (What Could Be Better Than Sliced Bread?): The Spec# Programming System
October 18, 2004
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.