Assume, Guarantee or Repair

Frenkel, Hadar and Grumberg, Orna and Pasareanu, Corina and Sheinvald, Sarai
(2020) Assume, Guarantee or Repair.
In: TACAS 2020.
Conference: TACAS Tools and Algorithms for Construction and Analysis of Systems

[img] Text
FGPS20.pdf

Download (311kB)

Abstract

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.

Actions

Actions (login required)

View Item View Item