CISPA
Browse
cispa_all_4028.pdf (303.99 kB)

Assume, Guarantee or Repair

Download (303.99 kB)
conference contribution
posted on 2024-02-29, 08:56 authored by Hadar FrenkelHadar Frenkel, Grumberg, Orna, Pasareanu, Corina, Sheinvald, Sarai
We present Assume-Guarantee-Repair (AGR) – a novel framework which not only verifies that a program satisfies a set of properties, but also repairs the program in case the verification fails. We consider communicating programs – these are simple C-like programs, extended with synchronous communication actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously. In every iteration, AGR either makes another step towards proving that the (current) system satisfies the specification, or alters the system in a way that brings it closer to satisfying the specification. We manage handling infinite-state systems by using a finite abstract representation, and reduce the semantic problems in hand – satisfying complex specifications that also contain first-order constraints – to syntactic ones, namely membership and equivalence queries for regular languages. We implemented our algorithm and evaluated it on various examples. Our experiments present compact proofs of correctness and quick repairs.

History

Preferred Citation

Hadar Frenkel, Orna Grumberg, Corina Pasareanu, Sarai Sheinvald. Assume, Guarantee or Repair. In: ACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems. 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

ACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems

Legacy Posted Date

2023-09-08

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_4028, author = {Hadar Frenkel AND Orna Grumberg AND Corina Pasareanu AND Sarai Sheinvald}, title = {Assume, Guarantee or Repair}, booktitle = {ACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems}, year = {2023} }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC