The L
∗ algorithm aims at learning a regular language U . Its entities consist of a teacher – an oracle
who answers membership queries (“is the word w in U ?”) and equivalence queries (“is A an automaton
whose language is U ?”), and a learner, who iteratively constructs a finite deterministic automaton A for U
by submitting a sequence of membership and equivalence queries to the teacher.
In using the L
∗ algorithm for learning an assumption A for the AG-rule, membership queries are answered according to the satisfaction of the specification P : If M 1 ||t satisfies P , then the trace t in hand
should be in A. Otherwise, t should not be in A. Once the learner constructs a stable system A, it submits
an equivalence query. The teacher then checks whether A is a suitable assumption, that is, whether M 1 ||A
satisfies P , and whether the language of M 2 is contained in the language of A. According to the results, the
process either continues or halts with an answer to the verification problem. The learning procedure aims at
learning the weakest assumption A w , which contains all the traces that in parallel with M 1 satisfy P . The
key observation that guarantees termination in [24] is that the components in this procedure – M 1 ,M 2 , P
and A w – are all regular.
Our setting is more complicated, since the traces in the components – both the programs and the specification – contain constraints, which are to be checked semantically and not syntactically. These constraints
may cause some traces to become infeasible. For example, if a trace contains an assignment x := 3 followed
by a constraint x ≥ 4 (modeling an “if” statement), then this trace does not contribute any concrete runs,
and therefore does not affect the system behavior. Thus, we must add feasibility checks to the process.
Constraints in the specification also pose a difficulty, as satisfiability of a specification is determined by
the semantics of the constraints and not only by the language syntax, and so there is more here to check
than standard language containment. Moreover, in our setting A w above may no longer be regular, see
Example 3. However, our method manages to overcome this problem.
As we have described above, not only do we construct a learning-based method for the AG-rule for
communicating programs, but we also repair the programs in case the verification fails. An AG-rule can
either conclude that M 1 ||M 2 satisfies P , or return a real, non-spurious counterexample of a computation t
of M 1 ||M 2 that violates P . In our case, instead of returning t, we repair M 2 in a way that eliminates this
counterexample. Our repair is both syntactic and semantic, where for semantic repair we use abduction [25]
to infer a new constraint which makes the counterexample t infeasible.
Consider again M 1 and P of Figure 2 and M 2 of Figure 1. The composition M 1 ||M 2 does not satisfy
P . For example, if the initial value of x pw is 2
63 , then after encryption the value of y pw is 2
64 , violating P .
Our algorithm finds a bad trace during the AG stage which captures this bad behavior, and the abduction in
the repair stage finds a constraint that eliminates it: x pw < 2
63 , and inserts this constraint to M 2 .
Following this step we now have an updated M 2 , and we continue with applying the AG-rule again,
using information we have gathered in the previous steps. In addition to removing the error trace, we update
the alphabet of M 2 with the new constraint.
Continuing our example, in a following iteration AGR will verify that the repaired M 2 together with
M 1 satisfy P , and terminate.
Thus, AGR operates in a verify-repair loop, where each iteration runs a learning-based process to determine whether the (current) system satisfies P , and if not, eliminates bad behaviors from M 2 while enriching
the set of constraints derived from these bad behaviors, which often leads to a quicker convergence. In case
the current system does satisfy P , we return the repaired M 2 together with an assumption A that abstracts
M 2 and acts as a smaller proof for the correctness of the system.
We have implemented a tool for AGR and evaluated it on examples of various sizes and of various
types of errors. Our experiments show that for most examples, AGR converges and finds a repair after 2-5
iterations of verify-repair. Moreover, our tool generates assumptions that are significantly smaller then the
(possibly repaired) M 2 , thus constructing a compact and efficient proof of correctness.
Assume, Guarantee or Repair
213
∗ algorithm aims at learning a regular language U . Its entities consist of a teacher – an oracle
who answers membership queries (“is the word w in U ?”) and equivalence queries (“is A an automaton
whose language is U ?”), and a learner, who iteratively constructs a finite deterministic automaton A for U
by submitting a sequence of membership and equivalence queries to the teacher.
In using the L
∗ algorithm for learning an assumption A for the AG-rule, membership queries are answered according to the satisfaction of the specification P : If M 1 ||t satisfies P , then the trace t in hand
should be in A. Otherwise, t should not be in A. Once the learner constructs a stable system A, it submits
an equivalence query. The teacher then checks whether A is a suitable assumption, that is, whether M 1 ||A
satisfies P , and whether the language of M 2 is contained in the language of A. According to the results, the
process either continues or halts with an answer to the verification problem. The learning procedure aims at
learning the weakest assumption A w , which contains all the traces that in parallel with M 1 satisfy P . The
key observation that guarantees termination in [24] is that the components in this procedure – M 1 ,M 2 , P
and A w – are all regular.
Our setting is more complicated, since the traces in the components – both the programs and the specification – contain constraints, which are to be checked semantically and not syntactically. These constraints
may cause some traces to become infeasible. For example, if a trace contains an assignment x := 3 followed
by a constraint x ≥ 4 (modeling an “if” statement), then this trace does not contribute any concrete runs,
and therefore does not affect the system behavior. Thus, we must add feasibility checks to the process.
Constraints in the specification also pose a difficulty, as satisfiability of a specification is determined by
the semantics of the constraints and not only by the language syntax, and so there is more here to check
than standard language containment. Moreover, in our setting A w above may no longer be regular, see
Example 3. However, our method manages to overcome this problem.
As we have described above, not only do we construct a learning-based method for the AG-rule for
communicating programs, but we also repair the programs in case the verification fails. An AG-rule can
either conclude that M 1 ||M 2 satisfies P , or return a real, non-spurious counterexample of a computation t
of M 1 ||M 2 that violates P . In our case, instead of returning t, we repair M 2 in a way that eliminates this
counterexample. Our repair is both syntactic and semantic, where for semantic repair we use abduction [25]
to infer a new constraint which makes the counterexample t infeasible.
Consider again M 1 and P of Figure 2 and M 2 of Figure 1. The composition M 1 ||M 2 does not satisfy
P . For example, if the initial value of x pw is 2
63 , then after encryption the value of y pw is 2
64 , violating P .
Our algorithm finds a bad trace during the AG stage which captures this bad behavior, and the abduction in
the repair stage finds a constraint that eliminates it: x pw < 2
63 , and inserts this constraint to M 2 .
Following this step we now have an updated M 2 , and we continue with applying the AG-rule again,
using information we have gathered in the previous steps. In addition to removing the error trace, we update
the alphabet of M 2 with the new constraint.
Continuing our example, in a following iteration AGR will verify that the repaired M 2 together with
M 1 satisfy P , and terminate.
Thus, AGR operates in a verify-repair loop, where each iteration runs a learning-based process to determine whether the (current) system satisfies P , and if not, eliminates bad behaviors from M 2 while enriching
the set of constraints derived from these bad behaviors, which often leads to a quicker convergence. In case
the current system does satisfy P , we return the repaired M 2 together with an assumption A that abstracts
M 2 and acts as a smaller proof for the correctness of the system.
We have implemented a tool for AGR and evaluated it on examples of various sizes and of various
types of errors. Our experiments show that for most examples, AGR converges and finds a repair after 2-5
iterations of verify-repair. Moreover, our tool generates assumptions that are significantly smaller then the
(possibly repaired) M 2 , thus constructing a compact and efficient proof of correctness.
Assume, Guarantee or Repair
213