Spec#
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.
Links
Watch a texternal pagealk about Spec#
Project Members
The project has been completed. Please contact Peter Müller in case of questions or comments.
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]
Acknowledgments
Spec# is a collaboration of many people. We have worked mostly with external pageRustan Leino, Microsoft Research.