Francesco Logozzo and Tom Ball
23 October 2012
We study the problem of suggesting code repairs at design time, based on the warnings issued by modular program verifiers. We introduce the concept of a verified repair, a change to a program's source that removes bad execution traces while increasing the number of good traces, where the bad/good traces form a partition of all the traces of a program. Repairs are property-specific. We demonstrate our framework in the context of warnings produced by the modular cccheck (a.k.a. clousot) abstract interpreter, and generate repairs for missing contracts, incorrect locals and objects initialization, wrong conditionals, buffer overruns, arithmetic overflow and incorrect floating point comparisons. We report our experience with automatically generating repairs for the .NET framework libraries, generating verified repairs for over 80% of the warnings generated by clousot.
|Published in||Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)|
Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo. Automatic Inference of Necessary Preconditions, Springer Verlag, January 2013.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
Francesco Logozzo and Matthieu Martel. Automatic Repair of Overflowing Expressions with Abstract Interpretation, Electronic Proceedings in Theoretical Computer Science, September 2013.
Francesco Logozzo. Practical Specification and Verification with CodeContracts, ACM, November 2013.
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.
Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.
Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.