CISPA
Browse
cispa_all_4027.pdf (438.49 kB)

Automated Program Repair Using Formal Verification Techniques

Download (438.49 kB)
chapter
posted on 2024-02-29, 08:56 authored by Hadar FrenkelHadar Frenkel, Grumberg, Orna, Rothenberg, Bat-Chen, Sheinvald, Sarai
We focus on two different approaches to automatic program repair, based on formal verification methods. Both repair techniques consider infinite-state C-like programs, and consist of a generate-validate loop, in which potentially repaired programs are repeatedly generated and verified. Both approaches are incremental – partial information gathered in previous verification attempts is used in the next steps. However, the settings of both approaches, including their techniques for finding repairs, are quite distinct. The first approach uses syntactic mutations to repair sequential programs with respect to assertions in the code. It is based on a reduction to the problem of finding unsatisfiable sets of constraints, which is addressed using an interplay between SAT and SMT solvers. A novel notion of must-fault-localization enables efficient pruning of the search space, without losing any potential repair. The second approach uses an Assume-Guarantee (AG) style reasoning in order to verify large programs, composed of two concurrent components. The AG reasoning is based on automata-learning techniques. When verification fails, the procedure repeatedly repairs one of the components, until a correct repair is found. Several different repair methods are considered, trading off precision and convergence to a correct repair.

History

Preferred Citation

Hadar Frenkel, Orna Grumberg, Bat-Chen Rothenberg, Sarai Sheinvald. Automated Program Repair Using Formal Verification Techniques. In: Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. 2023.

Primary Research Area

  • Reliable Security Guarantees

Legacy Posted Date

2023-09-08

Book Title

Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday

Publisher

Springer

Open Access Type

  • Unknown

BibTeX

@incollection{cispa_all_4027, author = {Hadar Frenkel AND Orna Grumberg AND Bat-Chen Rothenberg AND Sarai Sheinvald}, booktitle = {Automated Program Repair Using Formal Verification Techniques}, publisher = {Springer}, year = {2023} }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC