CISPA
Browse
cispa_all_3825.pdf (1.16 MB)

Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.

Download (1.16 MB)
journal contribution
posted on 2023-11-29, 18:05 authored by Hadar FrenkelHadar Frenkel, Orna Grumberg, Corina Pasareanu, Sarai Sheinvald
We present Assume-Guarantee-Repair (AGR) - a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs - these are simple C-like programs, extended with synchronous 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 required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.

History

Preferred Citation

Hadar Frenkel, Orna Grumberg, Corina Pasareanu and Sarai Sheinvald. Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.. In: International Journal on Software Tools for Technology Transfer. 2022.

Primary Research Area

  • Threat Detection and Defenses

Legacy Posted Date

2022-10-13

Journal

International Journal on Software Tools for Technology Transfer

Open Access Type

  • Gold

Sub Type

  • Article

BibTeX

@article{cispa_all_3825, title = "Assume, Guarantee or Repair - A Regular Framework for Non Regular Properties.", author = "Frenkel, Hadar and Grumberg, Orna and Pasareanu, Corina and Sheinvald, Sarai", journal="{International Journal on Software Tools for Technology Transfer}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC