Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk - Logozzo, Francesco (Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), 2011)
CodeContracts provide a language agnostic way to specify and check preconditions, postconditions and object invariants (collectively called contracts [17]). Speci cations take the form of calls to static methods of a Contract library [7]. The authoring library is available out-of-the-box to all .NET programmers from v4.