Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Modular and Verified Automatic Program Repair

Francesco Logozzo and Tom Ball

Abstract

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.

Details

Publication typeProceedings
Published inProceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12)
PublisherACM SIGPLAN

Newer versions

Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo. Automatic Inference of Necessary Preconditions, Springer Verlag, January 2013.

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. Practical Specification and Verification with CodeContracts, ACM, November 2013.

Previous versions

Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.

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.

> Publications > Modular and Verified Automatic Program Repair