Assume, Guarantee or Repair
Hadar Frenkel
1 , Orna Grumberg
1 , Corina Pasareanu
2 and Sarai Sheinvald
3
1 Department of Computer Science, The Technion, Haifa, Israel
2 Carnegie Mellon University and NASA Ames Research Center, CA, USA
3 Department of Software Engineering, Braude College of Engineering, Karmiel, Israel
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.
1 Introduction
Verification of large-scale systems is a main challenge in the field of formal verification. Often, the verification process of such a system does not scale well. Compositional verification aims to verify small
components of a system separately, and from the correctness of the individual components, to conclude the
correctness of the entire system. This, however, is not always possible, since the correctness of a component
often depends on the behavior of its environment.
The Assume-Guarantee (AG) style compositional verification [22,26] suggests a solution to this problem. The simplest AG rule checks if a system composed of components M 1 and M 2 satisfies a property P
by checking that M 1 under assumption A satisfies P and that any system containing M 2 as a component
satisfies A. Several frameworks have been proposed to support this style of reasoning. Finding a suitable
assumption A is then a common challenge in such frameworks.
In this work, we present Assume-Guarantee-Repair (AGR) – a fully automated framework which applies the Assume-Guarantee rule, and while seeking a suitable assumption A, incrementally repairs the
given program in case the verification fails. Our framework is inspired by [24], which presented a learningbased method to finding an assumption A, using the L
∗ [5] algorithm for learning regular languages.
Our AGR framework handles communicating programs. These are infinite-state C-like programs, extended with the ability to synchronously read and write messages over communication channels. We model
such programs as finite-state automata over an action alphabet, which reflects the program statements. The
accepting states in these automata model points of interest in the program that the specification can relate
to. The automata representation is similar in nature to that of control-flow graphs. Its advantage, however,
is in the ability to exploit an automata-learning algorithm such as L
∗ .
This research was partially supported by the Technion Hiroshi Fujiwara Cyber Security Research Center, the Israel
National Cyber Directorate and the Israel Science Foundation (ISF)
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 211–227, 2020.
https://doi.org/10.1007/978-3-030-45190-5_12
Hadar Frenkel
1 , Orna Grumberg
1 , Corina Pasareanu
2 and Sarai Sheinvald
3
1 Department of Computer Science, The Technion, Haifa, Israel
2 Carnegie Mellon University and NASA Ames Research Center, CA, USA
3 Department of Software Engineering, Braude College of Engineering, Karmiel, Israel
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.
1 Introduction
Verification of large-scale systems is a main challenge in the field of formal verification. Often, the verification process of such a system does not scale well. Compositional verification aims to verify small
components of a system separately, and from the correctness of the individual components, to conclude the
correctness of the entire system. This, however, is not always possible, since the correctness of a component
often depends on the behavior of its environment.
The Assume-Guarantee (AG) style compositional verification [22,26] suggests a solution to this problem. The simplest AG rule checks if a system composed of components M 1 and M 2 satisfies a property P
by checking that M 1 under assumption A satisfies P and that any system containing M 2 as a component
satisfies A. Several frameworks have been proposed to support this style of reasoning. Finding a suitable
assumption A is then a common challenge in such frameworks.
In this work, we present Assume-Guarantee-Repair (AGR) – a fully automated framework which applies the Assume-Guarantee rule, and while seeking a suitable assumption A, incrementally repairs the
given program in case the verification fails. Our framework is inspired by [24], which presented a learningbased method to finding an assumption A, using the L
∗ [5] algorithm for learning regular languages.
Our AGR framework handles communicating programs. These are infinite-state C-like programs, extended with the ability to synchronously read and write messages over communication channels. We model
such programs as finite-state automata over an action alphabet, which reflects the program statements. The
accepting states in these automata model points of interest in the program that the specification can relate
to. The automata representation is similar in nature to that of control-flow graphs. Its advantage, however,
is in the ability to exploit an automata-learning algorithm such as L
∗ .
This research was partially supported by the Technion Hiroshi Fujiwara Cyber Security Research Center, the Israel
National Cyber Directorate and the Israel Science Foundation (ISF)
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 211–227, 2020.
https://doi.org/10.1007/978-3-030-45190-5_12