Assume, Guarantee or Repair

(2020) Assume, Guarantee or Repair.

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference:	TACAS Tools and Algorithms for Construction and Analysis of Systems
Depositing User:	Hadar Frenkel
Date Deposited:	08 Sep 2023 13:47
Last Modified:	08 Sep 2023 13:47
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/4028

Actions

Actions (login required)

View Item