Spec# is a formal verification language that supports contract driven development / modular verification. Spec# was developed by Microsoft Research.
The Boogie verifier was part of the Spec# project.
Notes related to Spec# project
Papers related to Spec# project
- Specification and verification: The Spec# experience [barnett:cacm:2011]
- The Spec# programming system: An overview [barnett:cassis:2004]
- Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]
- The Spec# programming system: Challenges and directions [barnett:vstte:2005]
- Enforcing high-level protocols in low-level software [deline:pldi:2001]
- Behavioral interface specification languages [hatcliff:compsurv:2012]
- Reasoning about comprehensions with first-order SMT solvers [leino:sac:2009]