We present some extensions of a method for verifying safety properties of infinite state reactive systems. Safety properties are specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). In particular, we present a specialization strategy which is more general than previous proposals and we show, through some experiments performed on several infinite state reactive systems, that by using the specialized reachability programs obtained by our new strategy, we considerably increase the number of successful verifications. Then we show that the specialization time, the size of the specialized program, and the number of successful verifications may vary, depending on the polyvariance introduced by the specialization, that is, the set of specialized predicates which have been introduced. Finally, we propose a general framework for controlling polyvariance and we use our set of examples of infinite state reactive systems to compare in an experimental way various control strategies one may apply in practice.
Program specialization is a program transformation technique that, given a
program and a specific context of use, derives a specialized program that is more
effective in the given context [
Program specialization may generate polyvariant procedures, that is, it may derive, starting from a single procedure, multiple specialized versions of that procedure. In the case of (constraint) logic programming, program specialization may introduce several new predicates corresponding to specialized versions of a predicate occurring in the original program. The application of specialized procedures to specific input values often results in a very efficient computation. However, if the number of new predicate definitions and, hence, the size of the specialized program, is overly large, we may have difficulties during program compilation and execution.
In order to find an optimal balance between the degree of specialization and
the size of the specialized program, several papers have addressed the issue of
controlling polyvariance (see [
In this paper we address the issue of controlling polyvariance in the context
of specialization-based techniques for the automatic verification of properties of
reactive systems [
One of the present challenges in the verification field is the extension of
model checking techniques [
In order to overcome this limitation, several authors have advocated the use
of constraints to represent infinite sets of states and constraint logic programs
to encode temporal properties (see, for instance, [
The techniques based on abstract interpretation compute a conservative approximation of the program model, which is sometimes sufficient to prove that the property of interest actually holds. However, in the case where the property does not hold in the approximated model, one cannot conclude that the property does not hold.
The techniques based on program specialization transform the program that encodes the property of interest by taking into account the property to be proved and the initial states of the system, so that the construction of the model of the transformed program may terminate more often than the one of the original program, that is, the so-called verification precision is improved.
In this paper we show that the control of polyvariance plays a very relevant role in verification techniques based on program specialization. Indeed, the specialization time, the size of the specialized program, and the precision of verification may vary depending on the set of specialized predicates introduced by different specialization strategies. We also propose a general framework for controlling polyvariance during specialization and, through several examples of infinite state reactive systems taken from the verification literature, we compare in an experimental way various control strategies that may be applied in practice.
Our paper is structured as follows. In Section 2 we present a method based on constraint logic programming for specifying and verifying safety properties of infinite state reactive systems. In Sections 3 and 4 we present a general framework for specializing constraint logic programs that encode safety properties of infinite state reactive systems and, in particular, for controlling polyvariance during specialization. In Section 5 we present some experimental results. Finally, in Section 6 we compare our method with related approaches in the field of program specialization and verification. 2
An infinite state reactive system is specified as follows. A state is an n-tuple a1, . . . , an where each ai is either an element of a finite domain D or an element of the set R of the real numbers. By X we denote a variable ranging over states, that is, an n-tuple of variables X1, . . . , Xn where each Xi ranges over either D or R. Every constraint c is a (possibly empty) conjunction fd (c) of equations on a finite domain D and a (possibly empty) conjunction re(c) of linear inequations on R. An equation on R is considered as a conjunction of two inequations. Given a constraint c, every equation in fd (c) and every linear inequation in re(c) is said to be an atomic constraint.
The set I of the initial states is represented by a disjunction init1(X ) ∨ . . . ∨ initk(X ) of constraints on X . The transition relation is a disjunction t1(X, X ) ∨ . . . ∨ tm(X, X ) of constraints on X and X , where X is the n-tuple X1, . . . , Xn of primed variables.
A constraint c is also denoted by c(X ), when we want indicate that the variable X occurs in it. Similarly, for constraints denoted by c(X ) or c(X, X ). Given a constraint c and a tuple V of variables, we define the projection c|V to be the constraint d such that: (i) the variables of d are among the variables in V , and (ii) D ∪ R |= d ↔ ∃Z c, where Z is the tuple of the variables occurring in c and not in V . We assume that the set of constraints is closed under projection.
Given a clause C of the form H ← c ∧ G, by con(C) we denote the constraint c. A clause of the form H ← c, where c is a constraint, is said to be a constrained fact . We say that a constrained fact H ← c subsumes a clause H ← d ∧ G, where d is a constraint and G is a goal, iff d entails c, written d c, that is, D ∪ R |= ∀(d → c).
In this paper we will focus on the verification of safety properties. A safety property holds iff an unsafe state cannot be reached from an initial state of the system. The set U of the unsafe states is represented by a disjunction u1(X ) ∨ . . . ∨ un(X ) of constraints.
One can verify a safety property by one of the following two strategies: (i) the Backward Strategy: one applies a backward reachability algorithm, thereby computing the set BR of states from which it is possible to reach an unsafe state, and then one checks whether or not BR has an empty intersection with the set I of the initial states; (ii) the Forward Strategy: one applies a forward reachability algorithm, thereby computing the set FR of states reachable from an initial state, and then one checks whether or not FR has an empty intersection with the set U of the unsafe states.
Variants of these two strategies have been proposed and implemented in
various automatic verification tools [
The Backward and Forward Strategies can easily be encoded into constraint logic programming. In particular, we can encode the backward reachability algorithm by means of the following constraint logic program Bw :
I1: unsafe ← init1(X) ∧ bwReach(X)
· · · Ik: unsafe ← initk(X) ∧ bwReach(X) T1: bwReach(X) ← t1(X, X ) ∧ bwReach(X )
· · · Tm: bwReach(X) ← tm(X, X ) ∧ bwReach(X ) U1: bwReach(X) ← u1(X)
· · ·
Un: bwReach(X) ← un(X) We have that: (i) bwReach(X) holds iff an unsafe state can be reached from the state X in zero or more applications of the transition relation, and (ii) unsafe holds iff there exists an initial state of the system from which an unsafe state can be reached.
The semantics of program Bw is given by the least model, denoted M (Bw),
that is, the set of ground atoms derived by using: (i) the theory of equations
over the finite domain D and the theory of linear inequations over the reals R
for the evaluation of the constraints, and (ii) the usual least model construction
(see [
The system is safe if and only if unsafe ∈ M (Bw).
Example 1. Let us consider an infinite state reactive system where each state is a pair of real numbers and the following holds: (i) the set of initial states is the set of pairs X1, X2 such that the constraint X1 ≥ 1 ∧ X2 = 0 holds; (ii) the transition relation is the set of pairs of states X1, X2 , X1, X2 such that the constraint X1 = X1+X2 ∧ X2 = X2+1 holds; and (iii) the set of unsafe states is the set of pairs X1, X2 such that the constraint X2 > X1 holds.
For the above system the predicate unsafe is defined by the following CLP
program Bw 1:
1. unsafe ← X1 ≥ 1 ∧ X2 = 0 ∧ bwReach(X1, X2)
2. bwReach(X1, X2) ← X1 = X1 +X2 ∧ X2 = X2 +1 ∧ bwReach(X1, X2)
3. bwReach(X1, X2) ← X2 > X1
The Backward Strategy can be implemented by the bottom-up construction
of the least fixpoint of the immediate consequence operator SBw, that is, by
computing SBw ↑ ω [
One weakness of the Backward Strategy is that, when computing BR, it does not take into account the constraints holding on the initial states. This may lead to a failure of the verification process, even if the system is safe, because the computation of SBw ↑ ω may not terminate. A similar weakness is also present in the Forward Strategy as it does not take into account the properties holding on the unsafe states when computing FR.
In this paper we present a method, based upon the program specialization
technique introduced in [
The objective of program specialization is to transform the constraint logic program Bw into a new program SpBw such that: (i) unsafe ∈ M (Bw ) iff unsafe ∈ M (SpBw ), and (ii) the computation of SSpBw ↑ ω terminates more often than SBw ↑ ω because it exploits the constraints holding on the initial states.
Let us show how our method based program specialization works on the infinite state reactive system of Example 1.
Example 2. Let us consider the program Bw 1 of Example 1. The computation of SBw1 ↑ ω does not terminate, because it does not take into account the information about the set of initial states, represented by the constraint X1 ≥ 1 ∧ X2 = 0. (One can also check that the top-down evaluation of the query unsafe does not terminate either.)
This difficulty can be overcome by specializing the program Bw 1 with respect
to the constraint X1 ≥ 1 ∧ X2 = 0. Similarly to [
new q(X1, X2) ← X1 ≥ 1 ∧ X2 = k ∧ bwReach(X1, X2) where k gets the values 1, 2, . . . In order to terminate the specialization process we apply a generalization strategy and we introduce the following predicate definition which is a generalization of both clauses 4 and 7: 8. new 2(X1, X2) ← X1 ≥ 1 ∧ X2 ≥ 0 ∧ bwReach(X1, X2) We fold clause 6 using clause 8 and we get: 9. new 1(X1, X2) ← X1 ≥ 1 ∧ X2 = 0 ∧ X1 = X1 ∧ X2 = 1 ∧ new 2(X1, X2) Now we continue the transformation from the definition of the newly introduced predicate new 2. By unfolding clause 8 and then folding using again clause 8 we derive: 10. new 2(X1, X2) ← X1 ≥ 1 ∧ X2 ≥ 0 ∧ X1 = X1+X2 ∧ X2 = X2+1 ∧ new 2(X1, X2) 11. new 2(X1, X2) ← X1 ≥ 1 ∧ X2 > X1 The final specialized program, called SpBw 1, is made out of clauses 5, 9, 10, and 11. Now the computation of SSpBw1 ↑ ω terminates due to the presence of the constraint X1 ≥ 1 which holds on the initial states and occurs in all clauses of SpBw 1.
The form of the specialized program strongly depends on the strategy used for introduction of new predicates corresponding to the specialized versions of the predicate bwReach. For instance, in Example 1 we have introduced the two new predicates new 1 and new 2, and then we have obtained the specialized program by deriving mutually recursive clauses defining those predicates. Note, however, that the definition of new 2 is more general than the definition of new 1, because the constraint occurring in the body of the clause defining new 1 implies the constraint occurring in the body of the clause defining new 1. Thus, by applying an alternative strategy we could introduce new 2 only and derive a program SpBw 2 where clauses 5 and 9 are replaced by the following clause: 12. unsafe ← X1 ≥ 1 ∧ X2 = 0 ∧ new 2(X1, X2) Program SpBw 2 is smaller than SpBw 1 and the computation of SSpBw2 ↑ ω terminates in fewer steps than the one of SSpBw1 ↑ ω.
In general, when applying our specialization-based verification method there is an issue of controlling polyvariance, that is, of introducing a set of new predicate definitions that perform well with respect to the following objectives: (i) ensuring the termination and the efficiency of the specialization strategy, (ii) minimizing the size of the specialized program, and (iii) ensuring the termination and the efficiency of the fixpoint computation of the least models.
The objective of ensuring the termination of the fixpoint computation (and, thus, the precision of the verification\) can be in contrast with the other objectives, because it may need the introduction of less general predicates, while the achievement of other objectives is favoured by the introduction of more general predicates. In the next section we will present a framework for controlling polyvariance and achieving a good balance between the requirements we have listed above. 3
The core of our technique for controlling polyvariance is an algorithm for
specializing the CLP program Bw with respect to the constraints characterizing the
set of initial states. Our algorithm is generic, in the sense that it depends on
three unspecified procedures: (1) Partition, (2) Generalize, and (3) Fold. Various
definitions of the Partition, Generalize, and Fold procedures will be given in the
next section, thereby providing concrete specialization algorithms. These
definitions encode techniques already proposed in the specialization and verification
fields (see, for instance, [
Our generic specialization algorithm (see Figure 1) constructs a tree, called DefsTree, where: (i) each node is labelled by a clause of the form newp(X) ← d(X) ∧ bwReach(X), called a definition, defining a new predicate introduced during specialization, and (ii) each arc from node Di to node Dj is labelled by a subset of the clauses obtained by unfolding the definition of node Di. When no confusion arises, we will identify a node with its labelling definition. An arc from definition Di to definition Dj labelled by the set Cs of clauses is denoted
Cs by Di −→ Dj.
The definition at the root of DefsTree is denoted by the special symbol T. Initially, DefsTree is {T −{I→1} D1, . . . , T {−I→k} Dk}, where (i) I1, . . . , Ik are the clauses defining the predicate unsafe in program Bw (see Section 2), and (ii) for j = 1, . . . , k, Dj is the clause new j(X) ← initj(X) ∧ bwReach(X), such that new j is a new predicate symbol and the body of Dj is equal to the body of Ij.
A definition D in DefsTree is said to be recurrent iff D labels both a leaf node and a non-leaf node of DefsTree.
We construct the children of a non-recurrent definition D in the definition tree DefsTree constructed so far, as follows. We unfold D with respect to the atom bwReach(X) occurring in its body, that is, we replace bwReach(X) by the bodies of the clauses T1, . . . , Tm, U1, . . . , Un that define bwReach in Bw, thereby deriving a set UnfD of m + n clauses. Then, from UnfD we remove all clauses whose body contains an unsatisfiable constraint and all clauses that are subsumed by a (distinct) constrained fact in UnfD.
Next we apply the Partition procedure and we compute a set {B1, . . . , Bh} of pairwise disjoint sets of clauses, called blocks, such that UnfD = B1 ∪ . . . ∪ Bh.
Finally, we apply the Generalize procedure to each block of the partition.
This generalization step is often useful because, as it has been argued in [27],
it allows us to derive more efficient programs. Our Generalize procedure takes
as input the clause D, a block Bi of the partition of UnfD , and the whole
definition tree constructed so far. As we will indicate below, this third argument
of the Generalize procedure allows us to express the various techniques presented
in [
The output of the Generalize procedure is, for each block Bi, a definition Gi such that the constraint occurring in the body of Gi is entailed by every constraint occurring in the body of a non-unit clause (that is, a clause different from a constrained fact) in Bi and, hence, every non-unit clause in Bi can be folded using Gi. If all clauses in Bi are constrained facts (and thus, no folding step is required), then Gi is the special definition denoted by the symbol . If a clause in Bi has the form h(X ) ← c(X, X ) ∧ bwReach(X ), then Gi has the form newp(X ) ← d(X ) ∧ bwReach(X ) and c(X, X ) d(X ). However, we postpone the folding steps until the end of the construction of the whole tree DefsTree. For i = 1, . . . , h, we add to DefsTree the arc D −B→i Gi.
The construction of DefsTree terminates when all leaf clauses of the current
DefsTree are recurrent. In general, termination of this construction is not
guaranteed and it depends on the particular Generalize procedure one considers. All
Generalize procedures presented in the next section guarantee termination (see
also [
When the construction of DefsTree terminates we construct the specialized program SpBw by applying the Fold procedure which consists in: (i) collecting all clauses occurring in the blocks that label the arcs of DefsTree, and then (ii) folding every non-unit clause by using a definition that labels a node of DefsTree. Recall that, by construction, every non-unit clause occurring in a block that labels an arc of DefsTree can be folded by a definition that labels a node of DefsTree.
In the following Section, we will show how the specialization technique of Example 2 can be regarded as an instance of our generic specialization algorithm.
By using the correctness results for the unfolding, folding, and clause
removal rules (see, for instance, [
Theorem 1 (Correctness of the Specialization Algorithm). Let programs Bw and SpBw be the input and the output programs, respectively, of the specialization algorithm that uses any given Partition, Generalize, and Fold procedures. Then unsafe ∈ M (Bw) iff unsafe ∈ M (SpBw).
Input: Program Bw.
Output: Program SpBw such that unsafe ∈ M (Bw) iff unsafe ∈ M (SpBw). Initialization: DefsTree := {T {−I→1} D1, . . . , T {−I→k} Dk}; while there exists a non-recurrent definition D: newp(X) ← c(X) ∧ bwReach(X) in DefsTree do
Unfolding: UnfD := {newp(X) ← c(X) ∧ t1(X, X ) ∧ bwReach(X ), . . . , newp(X) ← c(X) ∧ tm(X, X ) ∧ bwReach(X ), newp(X) ← c(X) ∧ u1(X), . . . , newp(X) ← c(X) ∧ un(X) }; Clause Removal: while in UnfD there exist two distinct clauses E and F such that E is a constrained fact that subsumes F or there exists a clause F whose body has a constraint which is not satisfiable do UnfD := UnfD − {F } end-while; Definition Introduction: Partition(UnfD, {B1, . . . , Bh}); for i = 1, . . . , h do
Generalize(D, Bi, DefsTree, Gi);
DefsTree := DefsTree ∪ {D −B→i Gi} end-for ; end-while; Folding: Fold(DefsTree, SpBw)
In this section we provide several definitions of the Partition, Generalize, and Fold procedures used by the generic specialization algorithm. Let us start by introducing the following notions.
First, note that the set of all conjunctions of equations on D can be viewed as
a finite lattice whose partial order is defined by the entailment relation . Given
the constraints c1, . . . , cn, we define their most specific generalization, denoted
γ(c1, . . . , cn), the conjunction of: (i) the least upper bound of the conjunctions
fd (c1), . . . , fd (cn) of equations on D, and (ii) the convex hull [
Note that, for i = 1, . . . , n, ci γ(c1, . . . , cn). Given a set of constraints Cs = {c1, . . . , cn}, we define the equivalence relation fd on Cs such that, for every c1, c2 ∈ Cs, c1 fd c2 iff fd (c1) is equivalent to fd (c2) in D. We also define the equivalence relation re on Cs as the reflexive, transitive closure of the relation ↓R on Cs such that, for every c1, c2 ∈ Cs, c1 ↓R c2 iff re(c1) ∧ re(c2) is satisfiable in R.
For example, let us consider an element a ∈ D. Let c1 be the constraint X1 > 0 ∧ X2 = a and c2 be the constraint X1 < 0 ∧ X2 = a. Then we have that c1 fd c2 on {c1, c2}. Now, let c3 be the constraint X1 > 0 ∧ X1 < 2, c4 be the constraint X1 > 1 ∧ X1 < 3, and c5 be the constraint X1 > 2 ∧ X1 < 4. Since c3 ↓R c4 and c4 ↓R c5, we have c3 re c5 on {c3, c4, c5}. Note that c3 re c5 on {c3, c5} because c3 ∧ c5 is not satisfiable in R.
Partition. The Partition procedure takes as input the following set of n (≥ 1) clauses: UnfD := {C1 : newp(X ) ← c1(X, X ) ∧ bwReach(X ), · · · Cm : newp(X ) ← cm(X, X ) ∧ bwReach(X ), Cm+1 : newp(X ) ← cm+1(X, X ),
· · ·
Cn : newp(X ) ← cn(X, X ) } where, for some m, with 0 ≤ m ≤ n, C1, . . . , Cm are not constrained facts, and Cm+1, . . . , Cn are constrained facts. The Partition procedure returns as output a partition {B1, . . . , Bh} of UnfD, such that Bh = {Cm+1, . . . , Cn}. The integer h and the blocks B1, . . . , Bh−1 are computed by using one of the following partition operators. For the operators FiniteDomain, Constraint, and FDC, the integer h to be computed is obtained as a result of the computation of the blocks Bi’s. (i) Singleton: h = m+1 and, for 1 ≤ i ≤ h−1, Bi = {Ci}, which means that every non-constrained fact is in a distinct block; (ii) FiniteDomain: for 1 ≤ i ≤ h − 1, for j, k = 1, . . . , m, two clauses Cj and Ck belong to the same block Bi iff their finite domain constraints on the primed variables are equivalent, that is, iff cj |X fd ck|X on {c1|X , . . . , cm|X }; (iii) Constraint : for 1 ≤ i ≤ h−1, for i, j = 1, . . . , m, two clauses Cj and Ck belong to the same block Bi iff there exists a sequence of clauses in UnfD starting with Cj and ending with Ck such that for any two consecutive clauses in the sequence, the conjunction of the real constraints on the primed variables is satisfiable, that is, iff cj|X re ck|X on {c1|X , . . . , cm|X }; (iv) FDC : for 1 ≤ i ≤ h−1, for i, j = 1, . . . , m, two clauses Cj and Ck belong to the same block Bi iff they belong to the same block according to both the FiniteDomain and the Constraint partition operator, that is, iff cj |X fd ck|X and cj |X re ck|X on {c1|X , . . . , cm|X }; (v) All : h = 2 and B1 = {C1, . . . , Cm}, which means that all non-constrained facts are in a single block.
Generalize. The Generalize procedure takes as input a definition D, a block B of clauses computed by the Partition procedure, and the tree DefsTree of definitions introduced so far, and returns a definition clause G. If B is a set of constrained facts then G is the special definition denoted by the symbol . Otherwise, if B is the set {E1, . . . , Ek} of clauses and none of which is a constrained fact, then clause G is obtained as follows.
Step 1. Let b(X ) denote the most specific generalization γ(con (E1)|X , . . . ,
con(Ek)|X ).
if there exists a nearest ancestor A1 of D (possibly D itself) in DefsTree
such that A1 is of the form: newq(X ) ← a1(X ) ∧ bwReach(X ) (modulo
variable renaming) and a1(X ) fd con(D)
then banc(X ) = γ(a1(X ), b(X )) else banc(X ) = b(X );
Step 2. Let us consider a generalization operator (see [
In [
Widen. Given any two constraints c and d such that c is a1 ∧ . . . ∧ am, where the
ai’s are atomic constraints, the operator Widen, denoted W , returns the
constraint c W d which is the conjunction of the atomic constraints of c which
are entailed by d, that is, which are in the set {ah | 1 ≤ h ≤ m and d ah}
(see [
WidenSum. Let us first define the thin well-quasi ordering S. For any atomic
constraint a on R of the form q0 +kq1X1 +. . .+qkXk 0, where is either < or
≤, we define sumcoeff (a) to be j=0 |qj|. Given the two atomic constraints a1
of the form p1 < 0 and a2 of the form p2 < 0, we have that a1 S a2 iff
sumcoeff (a1) ≤ sumcoeff (a2). Similarly, if we are given the atomic constraints
a1 of the form p1 ≤ 0 and a2 of the form p2 ≤ 0. Given any two constraints c =
a1 ∧ . . . ∧ am and d = b1 ∧ . . . ∧ bn, where the ai’s and the bi’s are atomic
constraints, the operator WidenSum, denoted WS, returns the constraint
c WS d which is the conjunction of the constraints in the set {ah | 1 ≤ h ≤ m
and d ah} ∪ {bk | bk occurs in re(d) and ∃ ai occuring in re(c), bk S ai},
which is the set of atomic constraints which either occur in c and are entailed
by d, or occur in d and are less than or equal to some atomic constraint in c,
according to the thin well-quasi ordering S. Note that, in the case of our
Generalize procedure, we have that fd (d) is a subconjunction of c WS d.
Our generic Partition and Generalize procedures can be instantiated to get
known specialization algorithms and abstract interpretation algorithms. In
particular, (i) the technique proposed by Cousot and Halbwachs [
Fold. Let us first introduce the following definition. Given the two clauses C : newp(X ) ← c(X ) ∧ bwReach(X ) and D : newq(X ) ← d(X ) ∧ bwReach(X ), we say that C is more general than D, and by abuse of language, we write D C, iff d(X ) c(X ). A clause C is said to be maximally general in a set S of clauses iff for all clauses D ∈ S, if C D then D C. (Recall that the relation is not antisymmetric.) For the Fold procedure we have the following two options. Immediate Fold (Im, for short): (Step 1) all clauses occurring in the labels of the arcs of DefsTree are collected in a set F , and then (Step 2) for every non-unit clause E in F such that E occurs in the block Bi labelling an arc of the form D −B→i Di, for some clause D, E is folded using Di.
Maximally General Fold (MG, for short): (Step 1) is equal to that of Immediate Fold procedure, and (Step 2) every non-unit clause in F is folded using a maximally general clause in DefsTree.
Immediate Fold is simpler than Maximally General Fold, because it does not require any comparison between definitions in DefsTree to compute a maximally general one. Note also that a unique, most general definition for folding a clause may not exist, that is, there exist clauses that can be folded by using two definitions which are incomparable with respect to the ordering. However, the Maximally General Fold procedure allows us to use a subset of the definitions introduced by the specialization algorithm, thereby reducing polyvariance and deriving specialized programs of smaller size.
As already mentioned in the previous section, the specialization technique which we have applied in Example 2 can be obtained by instantiating our generic specialization algorithm using the following operators: Singleton for partitioning, Widen for generalization, and Immediate Fold for folding. 5
We have implemented the generic specialization algorithm presented in Section 3
using MAP [
We have performed the backward and forward reachability analyses of
several infinite state reactive systems taken from the literature [
For backward reachability we have applied the method presented in Section 2. For forward reachability we have applied a variant of that method and in particular, first, (i) we have encoded the forward reachability algorithm by a constraint logic program Fw and we have specialized Fw with respect to the set of the unsafe states, thereby deriving a new program SpFw, and then, (ii) we have computed the least fixpoint of the immediate consequence operator SSpFw (associated with program SpFw).
In Tables 1 and 2 we have reported the results of our verification experiments for backward reachability (that is, program Bw) and forward reachability (that is, program Fw), respectively. For each example of infinite state reactive system, we have indicated the total verification time (in milliseconds) of the non-specialized system and of the various specialized systems obtained by applying our strategy.
The symbol ‘∞’ means that either the program specialization or the least fixpoint construction did not terminate within 200 seconds. If the time taken is less than 10 milliseconds, we have written the value ‘0’. Between parentheses we have also indicated the number of predicate symbols occurring in the specialized program. This number is a measure of the degree of polyvariance determined by our specialization algorithm.
In the column named Input , we have indicated the time taken for computing the least fixpoint of the immediate consequence operator of the input, non-specialized program (whose definition is based on program Bw for backward reachability, and program Fw for forward reachability). In the six rightmost columns, we have shown the sum of the specialization time and the time taken for computing the least fixpoint of the immediate consequence operator of the specialized programs obtained by using the following six pairs of partition operators and generalization operators: (i) All, Widen , called All W , (ii) FDC, Widen , called FDC W , (iii) Singleton, Widen , called Single W , (iv) All, WidenSum , called All WS , (v) FDC, WidenSum , called FDC WS , and (vi) Singleton, WidenSum , called Single WS . For each example the tables have two rows corresponding, respectively, to the Immediate Fold procedure (Im) and Maximally General Fold procedure (MG).
If we consider precision, that is, the number of successful verifications, we have that the best combinations of the partition procedure and the generalization operators are: (i) FDC WS and Single WS for backward reachability, each of which verified 54 properties out of 58 (in particular, 27 with Im and 27 with MG), and (ii) Single WS for forward reachability, which verified 36 properties out of 58 (in particular, 18 with Im and 18 with MG).
If we compare the Generalize procedures we have that WidenSum is strictly more precise than Widen (up to 50%). Moreover, except for a few cases (backward reachability of CSM, forward reachability of Kanban), if a property cannot be proved by using WidenSum then it cannot be proved using Widen. WidenSum is usually more polyvariant than Widen. If we consider the verification times, they are generally favourable to WidenSum with respect to Widen, with some exceptions.
If we compare the partition operators we have that All is strictly less precise than the other operators: it successfully terminates in 138 cases out of 232 tests obtained by varying: (i) the given example-program, (ii) the property to be proved (either forward reachability or backward reachability), (iii) the generalization operator, and (iv) the Fold procedure. However, All is the only partition operator which allows us to verify the McCarty91 examples. By using the Singleton operator, the verification terminates in 158 cases out of 232, and by using the FDC operator, the verification successfully terminates in 159 cases out of 232. However, there are some properties (forward reachability of Peterson, InsertionSort and SelectionSort) which can only be proved using Singleton.
Note also that, if a property can be verified by using the FDC partition operator, then it can be verified by using either the operator All or the operator Singleton.
The two operators Singleton and FDC have similar polyvariance and verification times, while the operator All yields a specialized program with lower polyvariance and requires shorter verification times than Singleton and FDC.
If we compare the two Fold procedures, we have that Maximally General Fold for most of the examples has lower polyvariance and shorter verification times than Immediate Fold, while the precision of the two procedures is almost identical, except for a few cases where Maximally General Fold verifies the property, while Immediate Fold does not (backward reachability of Bakery4, Peterson and CSM). 6
We have proposed a framework for controlling polyvariance during the
specialization of constraint logic programs in the context of verification of infinite state
reactive systems. In our framework we can combine several techniques for
introducing a set of specialized predicate definitions to be used when constructing
the specialized programs. In particular, we have considered new combinations of
techniques introduced in the area of constraint-based program analysis and
program specialization such as convex hull, widening, most specific generalization,
and well-quasi orderings (see, for instance, [
We have performed an extensive experimentation by applying our specialization framework to the reachability analysis of infinite state systems. We have considered constraint logic programs that encode both backward and forward reachability algorithms and we have shown that program specialization improves the termination of the computation of the least fixpoint needed for the analysis. However, by applying different instances of our framework, we may get different termination results and different verification times. In particular, we have provided an experimental evidence that the degree of polyvariance has an influence on the effectiveness of our specialization-based verification method.
Our experiments confirm that, on one hand, a high degree of polyvariance often corresponds to high precision of analysis (that is, high number of terminating verifications) and, on the other hand, a low degree of polyvariance often corresponds to short verification times. We have also determined a specific combination of techniques for controlling polyvariance and provides, with respect to our set of examples, a good balance between precision and verification time.
Other techniques for controlling polyvariance during the specialization of
logic programs have been proposed in the literature [
Single W
All WS ∞ ∞ ∞ ∞ 19 21 ∞ ∞ ∞ ∞ 21 22 ∞ ∞ ∞ ∞ 21 23
Single W All WS
mentioned, the techniques presented in [
As a future work we plan to continue our experiments on a larger set of infinite state reactive systems so as to enhance and better evaluate the specialization framework presented here. We also plan to extend our approach to a framework for the specialization of constraint logic programs outside the context of verification of infinite state reactive systems.
This work has been partially supported by PRIN-MIUR and by a joint project between CNR (Italy) and CNRS (France). The last author has been supported by an ERCIM grant during his stay at LORIA-INRIA. Thanks to Laurent Fribourg and John Gallagher for many stimulating conversations. 26. C. Ochoa, G. Puebla, and M. V. Hermenegildo. Removing superfluous versions in polyvariant specialization of prolog programs. In Proceedings of LOPSTR ’05, Lecture Notes in Computer Science 3961, pages 80–97. Springer, 2006. 27. J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In Proceedings of LOPSTR ’02, Lecture Notes in Computer Science 2664, pages 90–108. Springer, 2003. 28. T. Yavuz-Kahveci and T. Bultan. Action Language Verifier: An infinite-state model checker for reactive software specifications. Formal Methods in System Design, 35(3):325–367, 2009.