Static Verification for Code Contracts

Manuel Fahndrich

Abstract

The Code Contracts project at Microsoft Research enables

programmers on the .NET platform to author specifications in

existing languages such as C# and VisualBasic. To take advantage of

these specifications, we provide tools for documentation generation, runtime

contract checking, and static contract verification.

This talk details the overall approach of the static contract checker and

examines where and how we trade-off soundness in order to obtain a

practical tool that works on a full-

edged object-oriented intermediate

language such as the .NET Common Intermediate Language.

Details

Publication typeInproceedings
Published inSAS'10 Proceedings of the 17th international conference on Static analysis
PublisherSpringer Verlag
> Publications > Static Verification for Code Contracts