Specification and Verification: The Spec# Experience

  • Mike Barnett ,
  • Manuel Fahndrich ,
  • Rustan Leino ,
  • Peter Muller ,
  • Wolfram Schulte ,
  • Herman Venter

Published by Association for Computing Machinery, Inc.

Spec# is a programming system that facilitates the development of correct software. The Spec# language extends C# with contracts that allow programmers to express their design intent in the code. The Spec# tool suite consists of a compiler that emits run-time checks for contracts, a static program verifier that attempts to mathematically prove the correctness of programs, and an integration into the Visual Studio development environment. Spec# shows how contracts and verifiers can be integrated seamlessly into the software development process. This paper reflects on the six-year history of the Spec# project, scientific contributions it has made, remaining challenges for tools that seek to establish program correctness, and prospects of incorporating verification into everyday software engineering.