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.