I will discuss the goals and the internals of Clousot, the static analyzer based on abstract interpretation that we have been developing at MSR in the last few years.

Clousot is the “official” static checker of the CodeContracts project. CodeContracts allow the programmer to specify Contracts (preconditions, postconditions and object invariant) in a language-agnostic way, without requiring any change in compiler, platform, IDE, … and in general to the usual routine professional programmer are so used to. Clousot integrates in the IDE and it is (fast enough to) run as a compilation step.

Unlike previous contract verifiers Clousot is not based on a theorem prover, but on abstract interpretation. This gives a set of advantages, the most important being:

• Automatic inference of sound loop invariants (no need for tedious programmer annotations)

• Predictability (the analysis follows the semantics of the program)

• Scalability (the analysis is tuned on the properties of interest)

Clousot can be downloaded for free as part of the CodeContracts tools at http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx (Commercial license) and http://research.microsoft.com/en-us/projects/contracts/ (Academic license).