Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Static contract checking with Abstract Interpretation

Manuel Fahndrich and Francesco Logozzo

Abstract

We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification of Contracts (precondition, postconditions and object invariants).

Clousot checks every method in isolation using an assume/guarantee reasoning: For each method under analysis Clousot assumes its precondition and asserts the postcondition. For each invoked method, Clousot asserts its precondition and assumes the postcondition. Clousot also checks the absence of common runtime errors, such as null-pointer errors, buffer or array overruns, divisions by zero, as well as less common ones such as checked integer overflows or floating point precision mismatches in comparisons. At the core of Clousot there is an abstract interpretation engine which infers program facts. Facts are used to discharge the assertions. The use of abstract interpretation (vs usual weakest precondition-based checkers) has two main advantages: (i) the checker automatically infers loop invariants letting the user focus only on boundary specifications; (ii) the checker is deterministic in its behavior (which abstractly mimics the flow of the program) and it can be tuned for precision and cost. Clousot embodies other techniques, such as iterative domain refinement, goal-directed backward propagation, precondition and postcondition inference, and message prioritization.

Details

Publication typeInproceedings
Published inProceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010)
PublisherSpringer Verlag

Previous versions

Francesco Logozzo and Manuel Fähndrich. Pentagons: A weakly relational domain for the efficient validation of array accesses, Association for Computing Machinery, Inc., March 2008.

Francesco Logozzo and Manuel Fähndrich. On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, Springer Verlag, 2008.

Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.

Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann. Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, IEEE, May 2009.

> Publications > Static contract checking with Abstract Interpretation