Main content

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 is based on ownership and 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.

Key Publications

  • M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter: Specification and Verification: The Spec# Experience
    Communications of the ACM, 2011. [PDF] [BIB]
  • P. Müller and J. N. Ruskiewicz: Using Debuggers to Understand Failed Verification Attempts
    Formal Methods (FM), 2011. [PDF] [BIB]
  • K. R. M. Leino and P. Müller: Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs
    Advanced Lectures on Software Engineering-LASER Summer School 2007/2008, 2010. [PDF] [BIB]
  • K. R. M. Leino, P. Müller, and A. Wallenburg: Flexible Immutability with Frozen Objects
    Verified Software: Theories, Tools, and Experiments (VSTTE), 2008. [PDF] [BIB]
  • K. R. M. Leino and P. Müller: Verification of Equivalent-Results Methods
    European Symposium on Programming (ESOP), 2008. [PDF] [BIB]
  • K. R. M. Leino and P. Müller: A verification methodology for model fields
    European Symposium on Programming (ESOP), 2006. [PDF] [BIB]
  • K. R. M. Leino and P. Müller: Object Invariants in Dynamic Contexts
    European Conference on Object-Oriented Programming (ECOOP), 2004. [PDF] [BIB]


Spec# is a collaboration of many people. We have worked mostly with Rustan Leino, Microsoft Research.

Page URL: http://www.pm.inf.ethz.ch/research/specsharp.html
Fri Jun 23 03:10:53 CEST 2017
© 2017 Eidgenössische Technische Hochschule Zürich