Manuel Fahndrich and Francesco Logozzo
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.
|Published in||Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010)|
Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.
Manuel Fahndrich and Francesco Logozzo. Checking Compatibility of Bit Sizes in Floating Point Comparison Operations, Electronic Proceedings in Theoretical Computer Science, September 2011.
Francesco Logozzo. Our Experience with the CodeContracts Static Checker, Springer, January 2012.
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.
Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett. An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, ACM SIGPLAN, 23 October 2012.
Francesco Logozzo and Matthieu Martel. Automatic Repair of Overflowing Expressions with Abstract Interpretation, Electronic Proceedings in Theoretical Computer Science, September 2013.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear. Verification Modulo Versions: Towards Usable Verification, ACM SIGPLAN, June 2014.
Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.
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.
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.
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.