Contributions To summarize, the main contributions of this paper are:
1. A learning-based Assume-Guarantee algorithm for infinite-state communicating programs, which manages to overcome the difficulties such programs present. In particular, our algorithm overcomes the inherent irregularity of the first-order constraints in these programs, and offers syntactic solutions to the
semantic problems they impose.
2. An Assume-Guarantee-Repair algorithm, in which the Assume-Guarantee and the Repair procedures
intertwine to produce a repaired program which, due to our construction, maintains many of the “good”
behaviors of the original program. Moreover, in case the original program satisfies the property, our
algorithm is guaranteed to terminate and return this conclusion.
3. An incremental learning algorithm that uses query results from previous iterations in learning a new
language with a richer alphabet.
4. A novel use of abduction to repair communicating programs over first order constraints.
5. An implementation of our algorithm, demonstrating the effectiveness of our framework.
Related Work Assume-guarantee style compositional verification [22,26] has been extensively studied.
The assumptions necessary for compositional verification were first produced manually, limiting the practicality of the method.
More recent works [9,16,14,6] proposed techniques for automatic assumption generation using learning and abstraction refinement techniques, making assume-guarantee verification more appealing. In [24,6]
alphabet refinement has been suggested as an optimization, to reduce the alphabet of the generated assumptions, and consequently their sizes. This optimization can easily be incorporated into our framework as
well.
Other learning-based approaches for automating assumption generation have been described in [7,17,8].
All these works address non-circular rules and are limited to finite state systems. Automatic assumption
generation for circular rules is presented in [12,13], using compositional rules similar to the ones studied
in [21,23].
Our approach is based on a non-circular rule but it targets complex, infinite-state concurrent systems,
and addresses not only verification but also repair. The compositional framework presented in [19] addresses
L
∗ -based compositional verification and synthesis but it only targets finite state systems.
Also related is the work in [18], which addresses automatic synthesis of circular compositional proofs
based on logical abduction; however the focus of that work is sequential programs, while here we target
concurrent programs. A sequential setting is also considered in [3], where abduction is used for automatically generating a program environment. Our computation of abduction is similar to that of [3]. However,
we require our constraints to be over a predefined set of variables, while they look for a minimal set.
The approach presented in [27] aims to compute the interface of an infinite-state component. Similar to our work, the approach works with both over- and under- approximations but it only analyzes one
component at a time. Furthermore, the component is restricted to be deterministic (necessary for the permissiveness check). In contrast we use both components of a system to compute the necessary assumptions,
and as a result they can be much smaller than in [27]. Furthermore, we do not restrict the components to be
deterministic and, more importantly, we also address the system repair in case of dissatisfaction.
2 Communicating Programs
In this section we present the notion of communicating programs. These are C-like programs, extended
with the ability to synchronously read and write messages over communication channels. We model such
programs as automata over an action alphabet that reflects the program statements. The alphabet includes
constraints, which are quantifier-free first-order formulas, representing the conditions in if and while statements. It also includes assignment statements and read and write communication actions. The automata
214
H. Frenkel et al.
1. A learning-based Assume-Guarantee algorithm for infinite-state communicating programs, which manages to overcome the difficulties such programs present. In particular, our algorithm overcomes the inherent irregularity of the first-order constraints in these programs, and offers syntactic solutions to the
semantic problems they impose.
2. An Assume-Guarantee-Repair algorithm, in which the Assume-Guarantee and the Repair procedures
intertwine to produce a repaired program which, due to our construction, maintains many of the “good”
behaviors of the original program. Moreover, in case the original program satisfies the property, our
algorithm is guaranteed to terminate and return this conclusion.
3. An incremental learning algorithm that uses query results from previous iterations in learning a new
language with a richer alphabet.
4. A novel use of abduction to repair communicating programs over first order constraints.
5. An implementation of our algorithm, demonstrating the effectiveness of our framework.
Related Work Assume-guarantee style compositional verification [22,26] has been extensively studied.
The assumptions necessary for compositional verification were first produced manually, limiting the practicality of the method.
More recent works [9,16,14,6] proposed techniques for automatic assumption generation using learning and abstraction refinement techniques, making assume-guarantee verification more appealing. In [24,6]
alphabet refinement has been suggested as an optimization, to reduce the alphabet of the generated assumptions, and consequently their sizes. This optimization can easily be incorporated into our framework as
well.
Other learning-based approaches for automating assumption generation have been described in [7,17,8].
All these works address non-circular rules and are limited to finite state systems. Automatic assumption
generation for circular rules is presented in [12,13], using compositional rules similar to the ones studied
in [21,23].
Our approach is based on a non-circular rule but it targets complex, infinite-state concurrent systems,
and addresses not only verification but also repair. The compositional framework presented in [19] addresses
L
∗ -based compositional verification and synthesis but it only targets finite state systems.
Also related is the work in [18], which addresses automatic synthesis of circular compositional proofs
based on logical abduction; however the focus of that work is sequential programs, while here we target
concurrent programs. A sequential setting is also considered in [3], where abduction is used for automatically generating a program environment. Our computation of abduction is similar to that of [3]. However,
we require our constraints to be over a predefined set of variables, while they look for a minimal set.
The approach presented in [27] aims to compute the interface of an infinite-state component. Similar to our work, the approach works with both over- and under- approximations but it only analyzes one
component at a time. Furthermore, the component is restricted to be deterministic (necessary for the permissiveness check). In contrast we use both components of a system to compute the necessary assumptions,
and as a result they can be much smaller than in [27]. Furthermore, we do not restrict the components to be
deterministic and, more importantly, we also address the system repair in case of dissatisfaction.
2 Communicating Programs
In this section we present the notion of communicating programs. These are C-like programs, extended
with the ability to synchronously read and write messages over communication channels. We model such
programs as automata over an action alphabet that reflects the program statements. The alphabet includes
constraints, which are quantifier-free first-order formulas, representing the conditions in if and while statements. It also includes assignment statements and read and write communication actions. The automata
214
H. Frenkel et al.