Specification and Verification: The Spec# Experience. - BARNETT, MIKE; FÄHNDRICH, MANUEL; LEINO, K. RUSTAN M.; MÜLLER, PETER; SCHULTE, WOLFRAM; VENTER, HERMAN (Communications of the ACM, 2011)
The article presents information on Spec#, pronounced speck sharp, a computer programming research project funded by software firm Microsoft. It is designed to help programmers deal with difficulties related to object-oriented languages, using a type system which distinguishes references that can never be null. The benefits which are made possible by the leveraging of a shared infrastructure are discussed in terms of online program verification systems and automatic theorem provers. An open source release of the Spec# project is described.