Lazy Constrained Monotonic Abstraction

Abstract

We introduce Lazy Constrained Monotonic Abstraction (lazy CMA for short) for lazily and soundly exploring well structured abstractions of infinite state non-monotonic systems. CMA makes use of infinite state and well structured abstractions by forcing monotonicity wrt. refinable orderings. The new orderings can be refined based on obtained false positives in a CEGAR like fashion. This allows for the verification of systems that are not monotonic and are hence inherently beyond the reach of classical analysis based on the theory of well structured systems. In this paper, we consistently improve on the existing approach by localizing refinements and by avoiding to trash the explored state space each time a refinement step is required for the ordering. To this end, we adapt ideas from classical lazy predicate abstraction and explain how we address the fact that the number of control points (i.e., minimal elements to be visited) is a priori unbounded. This is unlike the case of plain lazy abstraction which relies on the fact that the number of control locations is finite. We propose several heuristics and report on our experiments using our open source prototype. We consider both backward and forward explorations on non-monotonic systems automatically derived from concurrent programs. Intuitively, the approach could be regarded as using refinable upward closure operators as localized widening operators for an a priori arbitrary number of control points.

In part supported by the 12.04 CENIIT project.

1 Introduction

Well structured transition systems (WSTS:s for short) are maybe everywhere [17], but not all transition systems are well structured [3, 18]. Problems such as state reachability (e.g., safety) have been shown to be decidable for WSTS:s [2, 17]. This led to the development of algorithms that could check safety for systems ranging from lossy channels and Petri Nets to concurrent programs and broadcast protocols [19, 23, 25]. Many interesting examples of systems, including list manipulating programs [9], cache protocols [13] and mutex algorithms [1] are “almost” well structured in the sense that they would have been well structured if it was not for a number of transitions that violate the required assumptions. We build on the framework of Constrained Monotonic Abstraction (CMA for short) where we derive well structured abstractions for infinite state systems that are “almost” well structured.

To simplify, a WSTS comes with a well quasi ordering (wqo¹ for short) on the set of configurations. A key property of such systems is monotonicity: i.e., if a smaller configuration can fire a transition and get to some configuration c, then any configuration that is larger (wrt. the wqo) can also get to some configuration that is larger than c. In other words, larger configurations simulate smaller ones. Added to some assumptions on the effectivity of natural operations such as computing minimal elements and images of upward closed sets of configurations, it is possible to show the existence of sound and complete algorithms for checking the reachability of upward closed sets of configurations (i.e., coverability).

Systems where only some transitions are non monotonic can be approximated using WSTS:s by adding abstract transitions to restore monotonicity (monotonic abstraction). The resulting abstraction is also infinite state, and reachability of upward closed sets there is decidable. However, the obtained abstractions may fail to enforce invariants that are crucial for establishing unreachability of bad configurations in the original system. For instance, we explain in our recent work [18] how we automatically account for the number of processes synchronizing with (dynamic) barriers when establishing or refuting local (e.g., assertions) and global (e.g., deadlock freedom) properties of programs manipulating arbitrary many processes. Crucial invariants of such systems enforce an inherently non-monotonic behavior (e.g., a barrier transition that is enabled on a configuration is disabled if more processes are considered in a larger configuration).

Checking safety for such non-monotonic systems is not guaranteed to terminate without abstraction. Plain monotonic abstraction [1, 20] makes use of sets that are upward closed wrt. natural orderings as a sound symbolic representation. As stated earlier, this ensures termination if the used preorder is a wqo [2]. Of course, this comes at the price of possible false positives. In [3], we adapted existing counter example guided abstraction refinement (CEGAR) ideas to refine the ordering in plain monotonic abstraction. The preorder is strengthened by only relating configurations that happen to be in the same equivalence class, as defined by Craig interpolants obtained from the false positives. The new preorder is also a wqo, and hence, termination is again ensured. As implemented, the predicates are applied on all generated minimal elements to separate upward closed sets and the exploration has to restart from scratch each time a new refinement predicate is encountered.

We address these inefficiencies by adopting a lazy approach. Like in lazy predicate abstraction [21], we strive to localize the application of the refinement predicates and to reuse the explored state space. However, a major difference with plain lazy predicate abstraction is that the number of “control locations” (i.e., the locations to which subsets of the refinement predicates are mapped) is a priori unbounded (as opposed to the number of program locations of a non-parameterized system). We propose in this paper three heuristics that can be applied both in backward and in forward (something plain monotonic abstraction is incapable of). All three heuristics adopt a backtracking mechanism to reuse, as much as possible, the state space that has been explored so far. Schematically, the first heuristic (point-based) associates refinement predicates to minimal elements. The second heuristic (order-based) associates the refinement predicates to preorder related minimal elements. The third heuristic (descendants-based) uses for the child the preserved predicates of the parent. We describe in details the different approaches and state the soundness and termination of each refinement step. In addition, we experimentally compare the heuristics against each other and against the eager approach on our open source tool https://gitlab.ida.liu.se/apv/zaama.

Related Work. Coverability of non-monotonic systems is undecidable in general. Tests for zero are one source of non-monotonicy. The work in [8] introduces a methodology for checking coverability by using an extended Karp-Miller acceleration for the case of Vector Addition Systems (VAS:s for short) with at most one test for zero. Our approach is more general and tackles coverability and reachability for counter machines with arbitrary tests.

Verification methods can be lazy in different ways. For instance, Craig interpolants obtained from program runs can be directly used as abstractions [26], or abstraction predicates can be lazily associated to program locations [21]. Such techniques are now well established [5, 10, 27]. Unlike these approaches, we address lazy exploration for transition systems with “infinite control”. Existing WSTS based abstraction approaches do not allow for the possibility to refine the used ordering [23, 25], cannot model transfers for the local variables [16], or make use of accelerations without termination guarantees [7]. For example, in [23] the authors leverage on the combination of an exact forward reachability and of an aggressive backward approximation, while in [25], the explicit construction of a Petri Net is avoided.

The work in [24] gives a generalization of the IC3 algorithm and tries to build inductive invariants for well-structured transition systems. It is unclear how to adapt it to the kind of non-monotonic systems that we work with.

We believe the approach proposed here can be combined with such techniques. To the best of our knowledge, there is no previous work that considered making lazy the preorder refinement of a WSTS abstraction.

Outline. We start in Sect. 2 with some preliminaries. We then formalize targeted systems and properties in Sect. 3. We describe the adopted symbolic representation in Sect. 4 and go through a motivating example in Sect. 5. This is followed by a description of the eager and lazy procedures in Sect. 6. We finally report on our experiments in Sect. 7 and conclude in Sect. 8.

2 Preliminaries

We write $\mathbb {N}$ and $\mathbb {Z}$ to respectively mean the sets of natural and integer values. We let $\mathbb {B}=\{\texttt {tt},\texttt {ff}\}$ be the set of boolean values. Assume in the following a set $X$ of integer variables. We write ${\xi (X)}$ to mean the set of arithmetic expressions over $X$. An arithmetic expression $e$ in ${\xi (X)}$ is either an integer constant k, an integer variable $x$ in $X$, or the sum or difference of two arithmetic expressions. We write $e(X)$ to emphasize that only variables in $X$ are allowed to appear in $e$. We write $\texttt {atomsOf}(X)$ to mean the set of atoms over the variables $X$. An atom $\alpha$ is either a boolean $\texttt {tt}$ or $\texttt {ff}$ or an inequality $e\sim e'$ of two arithmetic expressions; where $\sim$ $\in \{<,\le ,\ge ,>\}$. We write $A$ to mean a set of atoms. Observe that the negation of an atom can be expressed as an atom. We often write $\psi$ to mean a conjunction of atoms, or conjunct for short, and use $\varPsi$ to mean a set of conjuncts. We use ${\varPi ({\xi (X)})}$ to mean arbitrary conjunctions and disjunctions of atoms over $X$. We can rewrite any presburger predicate over $X$ in negated normal form and replace the negated inequalities with the corresponding atoms to obtain an equivalent predicate $\pi _{}^{}$ in ${\varPi ({\xi (X)})}$. We write $\texttt {atomsOf}(\pi _{}^{})$ to mean the set of atoms participating in $\pi _{}^{}$.

A mapping $\mathbb {m}:U\rightarrow V$ associates an element in V to each element in U. We write to mean a partial mapping from U to V. We write $\texttt {dom}(\mathbb {m})$ and $\texttt {img}(\mathbb {m})$ to respectively mean the domain and the image of $\mathbb {m}$ and use for the mapping with an empty domain. We often write a partial mapping as the set $\{u\leftarrow \mathbb {m}(u)|~u\in \texttt {dom}(\mathbb {m})\}$ and write $\mathbb {m}\cup \mathbb {m}'$ to mean the union of two mappings $\mathbb {m}$ and $\mathbb {m}'$ with disjoint domains. Given a partial mapping , we write $\nu _{\mathbb {x}{}{}}(e)$ to mean the substitution in $e$ of $X$ variables by their respective $\mathbb {x}{}{}$ images and the natural evaluation of the result. As usual, $\nu _{\mathbb {x}{}{}}(e)$ is a well defined integer value each time $\mathbb {x}{}{}$ is a total mapping to $\mathbb {Z}$. This is generalized to (sets of) atoms, conjuncts and predicates.

We let $\mathbb {X}$ (resp. $\mathbb {X}_{\ge 0}$) be the set of all total mappings $X\rightarrow \mathbb {Z}$ (resp. $X\rightarrow \mathbb {N}$). We write $\mathbb {0}_X$ for the total mapping $X\rightarrow \{0\}$. The denotation of a conjunct $\psi$ over $\mathbb {X}$ (resp. $\mathbb {X}_{\ge 0}$), written $[\![\psi ]\!]_{\mathbb {X}}$ (resp. $[\![\psi ]\!]_{\mathbb {X}_{\ge 0}}$), is the set of all total mappings $\mathbb {x}{}{}$ in $\mathbb {X}$ (resp. in $\mathbb {X}_{\ge 0}$) s.t. $\nu _{\mathbb {x}{}{}}(\psi )$ evaluates to $\texttt {tt}$. We generalize to sets of atoms or conjuncts by taking the union of the individual denotations. Let $\unlhd$ be the preorder over $\mathbb {X}_{\ge 0}$ defined by $\mathbb {x}\unlhd \mathbb {x}'$ iff $\mathbb {x}(x)\le \mathbb {x}'(x)$ for each $x\in X$. Given a predicate $\pi _{}^{}$ in ${\varPi ({\xi (X)})}$, we say that a set $M\subseteq [\![\psi ]\!]_{\mathbb {X}_{\ge 0}}$ is minimal for $\psi$ if: (i) $\mathbb {x}\ntrianglelefteq \mathbb {x}'$ for any pair of different $\mathbb {x},\mathbb {x}'\in M$, and (ii) for any $\mathbb {x}'\in [\![\psi ]\!]_{\mathbb {X}_{\ge 0}}$, there is an $\mathbb {x}\in M$ s.t. $\mathbb {x}\unlhd \mathbb {x}'$. We recall the following facts from Linear Programming and [22].

Lemma 1

For a finite set of natural variables $X$, the preorder $\unlhd$ is a partial well quasi ordering. In addition, we can compute a finite and unique minimal set (written ${\texttt {min}_{\unlhd }(\pi _{}^{})}$) for any predicate $\pi _{}^{}$ in ${\varPi ({\xi (X)})}$.

Fig. 1.

The counter machine to the right captures the behaviour of the concurrent program to the left. It makes use of one counter per program location. It involves the following guarded commands: $\mathtt {gc_{ini}}::= (c_{0},c_{1},c_{2},c_{3},c_{4}:= 1,0,0,0,0)$, $\mathtt {gc_0}::= (c_{0}{}\ge 1 \Rightarrow c_{0}{}:=c_{0}+1)$, $\mathtt {gc_1}::= (c_{0}\ge 1 \Rightarrow c_{0},c_{1}:=c_{0}-1,c_{1}+1)$, $\mathtt {gc_2}::= (c_{1}\ge 1 \Rightarrow c_{1},c_{2}:=c_{1}-1,c_{2}+1)$, $\mathtt {gc_3}::= ((c_{2}\ge 1 \wedge c_{0}+c_{1}=0) \Rightarrow (c_{2},c_{3}:=c_{2}-1,c_{3}+1))$, $\mathtt {gc_4}::= (c_{3}\ge 1 \Rightarrow c_{3},c_{4}:=c_{3}-1,c_{4}+1)$, and ${\mathtt {gc_{err}}}: (c_{3}\ge 1)$. The resulting system is not well structured because of the zero test in $\mathtt {gc_3}$.

3 The State Reachability Problem

In this section, we motivate and formally define the reachability problem.

An Example. Consider the multi-threaded program to the left of Fig. 1 where only a single thread starts executing the program. A thread can spawn arbitrarily many concurrent threads with $\mathtt {t_0}$. Assume all threads asynchronously run the same program. Each thread can then set the shared flag $\mathtt {read}$ to $\mathtt {tt}$, and perform some reading followed by resetting $\mathtt {read}$ to $\mathtt {ff}$. All threads wait at the barrier. Obviously, $\mathtt {read}$ should be $\mathtt {ff}$ after the barrier since all threads that reached $\mathtt {pc_3}$ must have executed $\mathtt {t_2}$. The assertion at $\mathtt {pc_3}$ should therefore hold no matter how many threads are spawned. Capturing the barrier behaviour is crucial for establishing the non-violation of the assertion. The barrier behaviour is inherently non monotonic (adding more threads does not keep the barrier open). Our recent work [18] on combining different abstraction techniques can automatically generate non-monotonic counter machines such as the one to the right of Fig. 1. For this case, the assertion in the concurrent program is violated iff the target state is reachable in the counter machine. We explain briefly in the following how such counter machines are generated.

Our tool Pacman [18], takes as input multi-threaded programs similar to the one to left of Fig. 1. It automatically performs predicate, counter and monotonic abstractions on them and generates counter machines that overapproximate the behaviour of the original program. It then tries to solve the reachability problem for those machines.

Given a multi-threaded program, Pacman starts by generating concurrent boolean programs by performing predicate abstraction and incrementally improving it in a CEGAR loop [14]. This results in a boolean multi-threaded program that has the same control flow graph as the original program, but consists of only boolean variables. To the obtained boolean program, Pacman applies counter abstraction to generate a counter machine. Intuitively, each counter in the machine is associated to each local state valuation of a thread (that consists in the location and the valuation of the local variables of the thread). Each state in the machine is also associated to a valuation of shared variables. An extra state is reserved for the target. The statements of the boolean program are then translated as transitions in the counter machine.

For instance, in Fig. 1, counters $\mathtt {c_i}$, for $\mathtt {i: 0\le i \le 4}$, correspond respectively to the number of threads in program locations $\mathtt {pc_i}$ (the threads have no local variables here). Similarly, each transition $\mathtt {gc_i}$ is associated to each $\mathtt {t_i}$. Moreover, there are two additional transitions $\mathtt {gc_{ini}}$ and $\mathtt {gc_{err}}$ to model transitions involving initial or target states.

Note that the original multi-threaded program has non-monotonic invariants. For instance, transitions such as barriers, or any transition that tests variables representing the number of threads satisfying some property do not stay enabled if we add more threads. At the same time, the boolean concurrent programs generated above are inherently monotonic. This corresponds to a loss of precision. Thus, proving correctness of those programs whose correctness depends on respecting the non-monotonic behaviour (e.g., the one enforced by a barrier) can become impossible. As a remedy to this fact, Pacman automatically strengthens counter machine transitions by enforcing barrier invariants or by deriving new invariants (e.g., using an instrumented thread modular analysis) to regain some of the precision. This proved to help in verifying several challenging benchmarks. For example, consider the transition $\mathtt {t_3}$ in the program to the left of Fig. 1. At the moment a thread crosses the barrier first, there should be no thread before location $\mathtt {pc_2}$. This fact holds afterwards and forbids that a thread sets the flag $\mathtt {read}$ when some thread is checking the assertion. The transition $\mathtt {gc_3}$ is its corresponding transition in the strengthened counter machine. To ease the presentation of the example, $\mathtt {gc_3}$ is strengthened with the guard $\mathtt {(c_{0}+c_{1}=0)}$. (Observe that this is a simplification to ease the presentation; we can more faithfully capture the barrier by combining the test with a global flag.)

Counter machines. A counter machine is a tuple $(Q,C,A,\varDelta ,q_{init}^{},q_{trgt}^{})$ where $Q$ is a finite set of states, $C$ and $A$ are two distinct sets of counters (i.e., variables ranging over $\mathbb {N}$), $\varDelta$ is a finite set of transitions and $q_{init}^{}$ and $q_{trgt}^{}$ are two states in $Q{}{}$. A transition $\delta$ in $\varDelta$ is of the form $(q_{}^{},(grd \Rightarrow cmd),q'{}{})$ where $src(\delta )=q_{}^{}$ is the source state, $dst(\delta )=q'$ is the destination state and $\texttt {gc}(\delta )=(grd \Rightarrow cmd)$ is the guarded command. A guard $grd$ is a predicate in ${\varPi ({\xi (A\cup C)})}$ and a command $cmd$ is a multiple assignment $c_{1},\ldots ,c_{n}:= e_1,\ldots ,e_n$ that involves $e_1, \ldots e_n$ in ${\xi (A\cup C)}$ and pairwise different $c_{1}, \ldots c_{n}$ in $C$.

Semantics. A configuration is a pair $\theta =(q_{}^{},\mathbb {c})$ with the state $\texttt {st}(\theta )=q_{}^{}$ in $Q$ and the valuation $\texttt {val}(\theta )=\mathbb {c}$ in $\mathbb {C}_{\ge 0}:C\rightarrow \mathbb {N}$. We let $\varTheta$ be the set of configurations. We write $\theta \preceq \theta '$ to mean $\texttt {st}(\theta )=\texttt {st}(\theta ')$ and $\texttt {val}(\theta )\unlhd \texttt {val}(\theta ')$ (see Sect. 2). The relation $\preceq$ is a partial order over $\varTheta$. In fact, the pair $(\varTheta ,\preceq )$ is a partial well quasi ordering [22]. Given two configurations $(q_{}^{},\mathbb {c})$ and $(q',\mathbb {c}')$ and a transition $\delta \in \varDelta$ with $q_{}^{}=src(\delta )$, $q'=dst(\delta )$ and $\texttt {gc}(\delta )=(grd\Rightarrow (c_1, \ldots , c_n := e_1, \ldots , e_n))$, we write $(q_{}^{},\mathbb {c}) \xrightarrow []{\delta } (q',\mathbb {c}')$ to mean that there exists an $\mathbb {a}\in \mathbb {A}_{\ge 0}$ s.t. $\nu _{\mathbb {a}\cup \mathbb {c}}(grd)$ evaluates to $\texttt {tt}$ and $\mathbb {c}'(c_i)=\nu _{\mathbb {c}\cup \mathbb {a}}(e_i)$ for each $c_i$ in $C$. The auxiliary variables allow us to capture transfers (needed by predicate abstraction of concurrent programs). For instance, $(c_{0}\ge 1 \wedge c_{0}=a_0 \wedge c_{1}=a_1 \wedge a_0+a_1=a_2+a_3 ) \Rightarrow (c_{0},c_{1},c_{2},c_{3}:=0,0,a_2+c_{2},a_3+c_{3})$ captures situations where at least a thread is at $\mathtt {pc_{0}}$ and all threads at $\mathtt {pc_{0}}$ and $\mathtt {pc_{1}}$ move to $\mathtt {pc_{2}}$ and $\mathtt {pc_{3}}$. A run $\rho$ is a sequence $\theta _0 \theta _1 \cdots \theta _n$. We say that it covers the state $\texttt {st}(\theta _{n})$. The run is feasible if $\texttt {st}(\theta _0)=q_{init}^{}$ and $\theta _{i-1}{} \xrightarrow []{\delta _{i}} \theta _{i}$ for $i:1\le i \le n$. We write $\xrightarrow []{}$ for $\cup _{\delta \in \varDelta }\xrightarrow []{\delta }$.

Reachability. The reachability problem for a machine $(Q,C,A,\varDelta ,q_{init}^{},q_{trgt}^{})$ is to decide whether it has a feasible run that covers $q_{trgt}^{}$.

4 Symbolic Representation

Assume a machine $(Q,C,A,\varDelta ,q_{init}^{},q_{trgt}^{})$. We introduce (operations on) symbolic representations used in our reachability procedures in Sect. 6.

Boxes. A box $\mathbb {b}$ over a set $A$ of atoms is a partial mapping from $A$ to booleans $\mathbb {B}$. Intuitively, a box corresponds to a bitvector denoting an equivalence class in classical predicate abstraction. We use it to constrain the upward closure step. The predicate $\psi _{\mathbb {b}}$ of a box $\mathbb {b}$ is $\wedge _{\alpha \in \texttt {dom}(\mathbb {b})}((\mathbb {b}(\alpha )\wedge \alpha )\vee (\lnot \mathbb {b}(\alpha )\wedge \lnot \alpha ))$ ($\texttt {tt}$ is used for the empty box). Observe that this predicate is indeed a conjunct for any fixed box $\mathbb {b}$ and that $[\![\psi _{\mathbb {b}}]\!]$ does not need to be finite. We write $\mathbb {b}_{\texttt {tt}}$ for the box of the $\texttt {tt}$ conjunct. We will say that a box $\mathbb {b}$ is weaker than (or is entailed by) a box $\mathbb {b}'$ if $\psi _{\mathbb {b}'} \Rightarrow \psi _{\mathbb {b}}$ is valid. We abuse notation and write $\mathbb {b}\Leftarrow \mathbb {b}'$. Observe this is equivalent to $[\![\psi _{\mathbb {b}}]\!]\subseteq [\![\psi _{\mathbb {b}'}]\!]$.

Constraints. A constraint over a set $A$ of atoms is a triplet $\phi =(q_{}^{},\mathbb {c},\mathbb {b})$ where $\texttt {st}(\phi )\in Q$ is the state of the constraint, $\texttt {val}(\phi )=\mathbb {c}$ is its minimal valuation, and $\texttt {box}(\phi )=\mathbb {b}$ over $A$ is its box. We use $\varPhi$ to mean a set of constraints. A constraint $(q_{}^{},\mathbb {c},\mathbb {b})$ is well formed if $\nu _{\mathbb {c}}(\psi _{\mathbb {b}})$ holds. We only consider well formed constraints. We write $\texttt {clo}(\mathbb {c},\mathbb {b})$ to mean the conjunct $(\wedge _{c\in C}(c\ge \mathbb {c}(c))\wedge \psi _{\mathbb {b}})$. Intuitively, $\texttt {clo}(\mathbb {c},\mathbb {b})$ denotes those valuations that are both “in the box” and in the $\unlhd$-upward closure of $\mathbb {c}$. We let $[\![(q_{}^{},\mathbb {c},\mathbb {b})]\!]$ be the set $\{(q_{}^{},\mathbb {c}')|~\mathbb {c}'\in [\![\texttt {clo}(\mathbb {c},\mathbb {b})]\!]\}$. This set contains at least $(q_{}^{},\mathbb {c})$ by well formedness. Given two constraints $(q_{}^{},\mathbb {c},\mathbb {b})$ and $(q',\mathbb {c}',\mathbb {b}')$, we write $(q_{}^{},\mathbb {c},\mathbb {b}) \sqsubseteq (q',\mathbb {c}',\mathbb {b}')$ to mean that: (i) $q_{}^{}=q'$, and (ii) $\mathbb {c}\unlhd \mathbb {c}'$, and (iii) $\mathbb {b}\Leftarrow \mathbb {b}'$. Observe that $\phi \sqsubseteq \phi '$ implies $[\![\phi ']\!]\subseteq [\![\phi ]\!]$. A subset $\varPhi$ of a set of constraints $\varPhi '$ is minimal if: (i) $\phi _1\not \sqsubseteq \phi _2$ for any pair of different constraints $\phi _1,\phi _2\in \varPhi$, and (ii) for any $\phi '\in \varPhi '$, there is a $\phi \in \varPhi$ s.t. $\phi \sqsubseteq \phi '$.

Lemma 2

For a finite set of atoms $A$ over $C$, the ordering $\sqsubseteq$ is a well quasi ordering over the set of well formed constraints over $A$. In addition, we can compute, for any set $\varPhi$ of constraints, a finite $\sqsubseteq$-minimal subset $\texttt {min}_{\sqsubseteq }(\varPhi )$.

Image Computations. Assume a conjunct $\psi$ over $C$ and a guarded command $gc=(grd \Rightarrow cmd)$ for some $\delta \in \varDelta$. Recall that $grd$ is in ${\varPi ({\xi (C\cup A)})}$ and that $cmd$ is of the form $c_1,\ldots ,c_n:=e_1,\ldots ,e_n$ where, for each $i:1\le i\le n$, $c_i$ is in $C$ and $e_i$ is also in ${\xi (C\cup A)}$. We let $L'$ be the set of primed versions of all variables appearing in the left hand side of $cmd$. We write ${\texttt {pre}}_{gc}(\psi )$ to mean a set of conjuncts whose disjunction is equivalent to $(\exists A\cup L'. ( \wedge _{1\le i\le n} (c'_i=e_i)\wedge grd\wedge \psi [\{c\leftarrow c'|~c'\in L'\}]))$. We also write ${\texttt {post}}_{gc}(\psi )$ to mean a set of conjuncts whose disjunction is equivalent to $(\exists A\cup C. (\wedge _{1\le i\le n} (c'_i=e_i)\wedge grd\wedge \psi ))[\{c'\leftarrow c|~c\in C\}]$. We naturally extend ${\texttt {pre}}_{gc}(\psi )$ and ${\texttt {post}}_{gc}(\psi )$ to sets of conjuncts.

Lemma 3

Assume $\delta \in \varDelta$ and conjuncts $\varPsi$. We can compute ${\texttt {pre}}_{\texttt {gc}(\delta )}(\varPsi )$ and ${\texttt {post}}_{\texttt {gc}(\delta )}(\varPsi )$ s.t. (resp. $[\![{\texttt {post}}_{\texttt {gc}(\delta )}(\varPsi )]\!]$) equals $\{\mathbb {c}|~(src(\delta ),\mathbb {c})\xrightarrow []{\delta }(dst(\delta ),\mathbb {c}') \text { with } \mathbb {c}'\in [\![\varPsi ]\!]\}$ (resp. $\{\mathbb {c}'|~(src(\delta ),\mathbb {c})\xrightarrow []{\delta }(dst(\delta ),\mathbb {c}') \text { with } \mathbb {c}\in [\![\varPsi ]\!]\}$).

Grounded Constraints and Symbolic Sets. A grounded constraint is a pair $\gamma =((q_{}^{},\mathbb {c},\mathbb {b}),\psi )$ that consists of a constraint $\texttt {cstrOf}(\gamma )=(q_{}^{},\mathbb {c},\mathbb {b})$ and a conjunct $\texttt {groundOf}(\gamma )=\psi$. It is well formed if: $(q_{}^{},\mathbb {c},\mathbb {b})$ is well formed, $\psi \Rightarrow \texttt {clo}(\mathbb {c},\mathbb {b})$ is valid, and $\mathbb {c}\in [\![\psi ]\!]$. We only manipulate well formed grounded constraints. Intuitively, the ground $\psi$ in $((q_{}^{},\mathbb {c},\mathbb {b}),\psi )$ represents the “non-approximated” part of the $\unlhd$-upward closure of $\mathbb {c}$. This information will be needed for refining the preorder during the analysis. We abuse notation and write $\texttt {cstrOf}(\varGamma )$, resp. $\texttt {groundOf}(\varGamma )$, to mean the set of constraints, resp. grounds, of a set $\varGamma$ of grounded constraints. A trace $\sigma _{}^{}$ of length n is a sequence starting with a grounded constraint followed by n transitions and grounded constraints. We say that two traces $(\phi _0,\psi _0)\cdot \delta _1\cdot (\phi _1,\psi _1)\cdots \delta _n\cdot (\phi _n,\psi _n)$ and $(\phi '_0,\psi '_0)\cdot \delta '_1\cdot (\phi '_1,\psi '_1)\cdots \delta '_{n'}\cdot (\phi '_{n'},\psi '_{n'})$ are equivalent if: (i) $n=n'$, and (ii) $\delta _i$ is the same as $\delta '_i$ for each $i: 1\le i \le n$, and (iii) $\phi _i \sqsubseteq \phi '_i$, $\phi '_i \sqsubseteq \phi _i$ and $\psi _i \Leftrightarrow \psi '_i$ for each $i: 0\le i \le n$. A symbolic set is a set of pairs of grounded constraints and traces. Given a symbolic set T, we also use $\texttt {cstrOf}(T)$ to mean all constraints $\phi$ appearing in some $((\phi ,\psi ),\sigma _{}^{})$ in T. Recall that we can compute a set $\texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(T))$ of $\sqsubseteq$-minimal constraints for $\texttt {cstrOf}(T)$.

5 An Illustrating Example

We use the example introduced in Sect. 3 to give an intuition of the lazy heuristics described in this paper. A more detailed description follows in Sect. 6.

Plain monotonic abstraction proceeds backwards while systematically closing upwards wrt. the natural ordering $\preceq$ on $\varTheta$. The trace depicted in Fig. 2 is a generated false positive. In this description, for $i:0\le i\le 7$, we write $\gamma _i=(\phi _i,\psi _i)$ to mean the grounded constraint with the grounded constraint $\psi _i$ and the constraint $\phi _i=(q_{i}^{},\mathbb {c}_i,\mathbb {b}_i)$. Intuitively, the grounded constraint represents “exact” valuations while the constraint captures over-approximations that are of the form $(q_{i}^{},\mathbb {c})$ where $\mathbb {c}_i\unlhd \mathbb {c}$ and $\mathbb {c}$ satisfies $\psi _{\mathbb {b}_i}$. The computation starts from the grounded constraint $\gamma _7=((\mathtt {trgt},\mathbb {c}_7,\mathbb {b}_{\texttt {tt}}),\psi _7)$ where $\psi _7$ is $\wedge _{c\in C}(c\ge 0)$ (always implicit). For $\gamma _7$, the exact and the over-approximated parts coincide.

The trace then computes $\psi _6=(c_{3}\ge 1)$ which captures the valuations of the predecessors of $(\mathtt {trgt},\mathbb {c}_7,\mathbb {b}_{\texttt {tt}})$ wrt. $(\mathtt {rd},\mathtt {gc_{err}},\mathtt {trgt})$. This set happens to be upward closed and there is no need for approximation, hence $\gamma _6=((\mathtt {rd},\mathbb {c}_6,\mathbb {b}_{\texttt {tt}}),\psi _6)$. Valuations of the exact predecessors of $(\mathtt {rd},\mathbb {c}_6,\mathbb {b}_{\texttt {tt}})$ wrt. $(\mathtt {rd},\mathtt {gc_3},\mathtt {rd})$ are captured with the conjunct $\psi _5=(c_{0}=c_{1}=0 \wedge c_{2}\ge 1)$. These are approximated with the conjunct $(c_{0}\ge 0 \wedge c_{1}\ge 0 \wedge c_{2}\ge 1)$. Continuing to compute the predecessors and closing upwards leads to the constraint $\phi _0$ which involves the initial state $\mathtt {init}$. The trace is reported as a possible reachability witness. It is well known [4] that upward closed sets are not preserved by non-monotonic transitions (such as those involving $\mathtt {gc_3}$ in Fig. 1). At the same time, maintaining an exact analysis makes guaranteeing termination impossible.

Following the trace in forward from the left, it turns out that the upward closure that resulted in $\gamma _5$ is the one that made the spurious trace possible. Indeed, it is its approximation that allowed the counter $c_{1}$ to be non zero. This new value for $c_{1}$ is the one that allowed the machine to execute $(\lnot \mathtt {rd},\mathtt {gc_{1}},\mathtt {rd})$ in backward from $\phi _5$, making reaching the initial state possible. The constraint $\phi _5$ is the pivot constraint of the trace. Constrained monotonic abstraction (CMA) proposes to refine the used ordering by strengthening it with a relevant predicate. In this case, $c_{1}\le 0$ is used for strengthening, but in general (the atoms of) any predicate in ${\varPi ({\xi (C)})}$ that separates the exact predecessors from the reachable part of the upward closure would do.

Fig. 2.

A spurious trace generated by monotonic abstraction. The $\gamma _5$ constraint introduces the first over-approximation that makes the spurious trace possible. The configuration $(\mathtt {rd},\mathbb {c}_5)$ is the pivot configuration of the spurious trace.

Eager CMA. Introduced in [3]. The exploration is restarted from scratch and $(c_{1}\le 0)$ is used to systematically partition all exact predecessors. The upward closure is constrained to not alter the refinement predicate. All generated valuations are therefore approximated with the stronger ordering. Localizing refinement can make possible both reusing a potentially large part of the explored state space and applying the (slower) refinement to a smaller number of sets.

Lazy CMA. When backtracking, we only eliminate those constraints that were obtained as descendants of a constraint that needs to be refined. We refer to this constraint as the pivot constraint, and to its minimal configuration as the pivot configuration. In fact, we identify three localization heuristics:

• point-based-lazy. We map the refinement predicates to the pivot configurations. Later in the exploration, when we hit a new pivot configuration, we constrain wrt. those predicates that were already mapped to it.

• order-based-lazy. The point-based approach may be too localized as there is an infinite number of pivot configurations. For instance, a similar trace can continue, after $(\mathtt {rd},c_{2}=1)$, with $\mathtt {gc_{1}}$ and get to the minimal configuration sending $c_{2}$ to 2. This one is different from the mapped pivot configuration, and hence we need to introduce a new pivot configuration with the same predicate $c_{0}\le 0$. This approach considers the predicates of all larger or smaller pivot configurations. The idea being that, if the predicate was important for the mapped pivot configuration, then it must have been to separate it from a reachable upward closed part, and hence it may be relevant.

• descendants-based-lazy. In addition to associating refinement predicates to pivot configurations as in the point-based approach, this heuristic leverages on the fact that predicates may remain relevant for a sequence of transitions. Here we compare the exact predecessors with the predicates used to constrain the upward closure of the parent. If those predicates still hold for the predecessors, then we maintain them when closing upwards. This heuristic bears similarity to forward propagation of clauses in IC3 [24], as in the IC3 algorithm the clauses are propagated in the trace from a preceding formula to the succeeding one if they still hold.

6 State Reachability Checking

We describe in this section four different forward CMA variants (eager, point-based-lazy, order-based-lazy and descendants-based-lazy). The four procedures can also be applied in backwards (as described in the experiments of Sect. 7). The four variants use grounded constraints as symbolic representations for possibly infinite numbers of machine configurations. The symbolic representation is refined using atoms obtained using a counterexample guided refinement scheme. The difference between the four variants lays in the way discovered predicates (in fact atoms for simplifying the presentation) are associated to the new symbolic representations and in the way backtracking is carried out. We start by introducing the basic “partition” procedure.

Partition. “partition$(q_{}^{}, \psi , A)$” partitions $\psi$ according to all atoms in $A$. Each obtained conjunct is further decomposed according to its $\unlhd$-minimal valuations. Conjuncts are then used to build a well formed grounded constraint $((q_{}^{},\mathbb {c},\mathbb {b}), \psi ')$ where $\mathbb {b}$ is a box over $A$. Observe that the disjunction of the grounds of the obtained grounded constraints is equivalent to $\psi$. Soundness is stated in Lemma 4.

Lemma 4

Assume a finite set $A$ of atoms. For any conjunct $\psi$, it is the case that $[\![(q_{}^{},\psi )]\!] = \{(q_{}^{},\mathbb {c})|~\mathbb {c}\in [\![\psi ']\!]_{\ge 0}\text { for each } \psi ' \in \texttt {groundOf}(\mathrm {partition})(q, \psi , A))\} \subseteq [\![\texttt {cstrOf}(\mathrm {partition})(q, \psi , A))]\!]$.

Eager CMA, like the other variants, starts by passing a description of the machine to the “checkReachability” procedure. It returns a feasible run covering $q_{trgt}^{}$, or states that there are no such runs. The procedure returns directly (line 1) if initial and target states coincide. It then calls “partition” to obtain a set of well formed grounded constraints that together capture all initial configurations. These are passed to the “explore” procedure.

Explore. “explore$(M,\mathtt {work},\mathtt {store},\mathtt {sleep},\mathbb {f})$” results in a working list process that maintains three symbolic sets $\mathtt {work}$, $\mathtt {store}$ and $\mathtt {sleep}$. The last is only relevant for the lazy variants. The partial mapping encapsulates all refinement predicates discovered so far and is therefore empty when the procedure is called from “checkReachability”. Intuitively, $\mathbb {f}(\theta )$ associates to the pivot configuration $\theta$ those predicates that helped eliminate a false positive when $\theta$ was the minimal configuration of the constraint that made the false positive possible. We will explain how $\mathbb {f}$ is updated when introducing the procedure “simulate”. The symbolic set $\mathtt {work}$ is used for the grounded constraints that are yet to be visited (i.e., for which the successors are still to be computed and approximated). The $\mathtt {store}$ set is used for both those grounded constraints that have been visited and for those in working. The $\mathtt {sleep}$ set corresponds to those constraints that might have to be visited but for which there is an $\sqsubseteq$-equivalent representative in $\mathtt {store}$. In case a backtracking eliminates the representative in $\mathtt {store}$, the corresponding grounded constraint in $\mathtt {sleep}$ has to be reconsidered. This is explained in the “backtrack” procedure of the lazy variants.

The procedure picks a pair $((\phi ,\psi ),\sigma _{}^{})$ from $\mathtt {work}$ and $\texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(\mathtt {store}))$. If the initial state is reached, it calls procedure “simulate” to check the associated trace and to backtrack if needed (lines 4–5). Otherwise, we start by iterating through all transitions $\delta$ in $\varDelta$ and compute an exact representation of the predecessors of the constraint. The call “$decompose (q_{}^{},\psi _p,\mathbb {f},\mathbb {b})$” boils down, for the eager variant, to a call to “partition$(q_{}^{},\psi _p,\texttt {img}(\mathbb {f}))$”. The obtained grounded constraints are used to update the $\mathtt {store},\mathtt {work}$ and $\mathtt {sleep}$ symbolic sets.

If there was no pair picked at line 1, then we have finished the exploration and return $unreachable$. In fact, pairs are never removed from $\mathtt {store}$ if no target states are encountered at line 4. In addition, two pairs with $\sqsubseteq$-equivalent constraints cannot be added to $\mathtt {work}$ (lines 10–13). For this reason, executing the first line an infinite number of times without calling procedure “simulate” would result in an infinite sequence of constraints that would violate Lemma 2.

Simulate. This procedure checks feasibility of a trace $\sigma _{}^{}$ from $q_{init}^{}$ to $q_{trgt}^{}$. The procedure incrementally builds a sequence of sets of conjuncts $\varPsi _n, \ldots , \varPsi _{0}$ where each $\varPsi _i$ intuitively denotes the valuations that are backwards reachable from $q_{trgt}^{}$ after k steps of $\sigma _{}^{}$ (starting from $k=0$), and are still denoted by $\texttt {clo}(\mathbb {c}_{(n-k)},\mathbb {b}_{(n-k)})$. The idea is to systematically intersect (a representation of) the successors of step k with the grounded constraint that gave raise to the constraint at step $k+1$. If the procedure finds a satisfiable $\varPsi _0$, then a run can be generated by construction. Such a run is then returned at line 8. Otherwise, there must have been a step where the “exact” set of conjuncts does not intersect the conjunct representing the exact part that gave raise to the corresponding constraint. In other words, the trace could be eliminated by strengthening the over-approximation at line 7 of the “explore” procedure. In this case, (at line 6 of the “simulate” procedure), new refinement atoms are identified using an off-the-shelf interpolation procedure for QF_LIA (Quantifier Free Linear Arithmetic). This information will be used differently by the eager and lazy variants when calling their respective “backtrack” procedures.

Eager backtracking throws away the explored state space (line 1) and restarts the computation from scratch using the new refinement atoms captured in $\mathbb {f}$.

Lazy Backtracking. Intuitively, all three lazy approaches reuse the part of the explored state space that is not affected by the new refinements. This is done by restarting the exploration from new sets $\mathtt {work}$ and $\mathtt {store}$ that are obtained after pruning away the pivot constraint identified by the argument i passed by “simulate” together with all its descendants (identified in lines 1–6). One important aspect is that grounded constraints that have not been added to $\mathtt {store}$ at line 11 of the “explore” procedure may have been discarded for the wrong reason (i.e., there was an $\sqsubseteq$-equivalent constraint that needs to be pruned away now). This would jeopardize soundness. For this reason we maintain the $\mathtt {sleep}$ set for tracking the discarded grounded constraints that have to be put back to $\mathtt {work}$ and $\mathtt {store}$ if the constraint that blocked them is pruned away (see lines 4–6). The refined pivot is added to the new sets $\mathtt {work}$ and $\mathtt {store}$ (lines 10–13). Lines 7–9 are only used by the descendants-based approach which takes into account the box of the parent.

The main difference between the lazy variants is in the way their respective “decompose” procedures associate refinement atoms to “exact” conjuncts.

Point-based. This variant is the one that “localizes” most the refinement. Each time an obtained grounded conjunct is considered for approximation, it checks whether its minimal valuation has already been associated to some refinement atoms. If it is the case, it passes them when calling the “partition” procedure.

Order-based. This variant “localizes” less than the point-based variant. Each time an obtained “exact” conjunct is considered for approximation, it checks whether its minimal valuation is $\unlhd$-related to an already mapped valuation. The union of all corresponding atoms is passed to the “partition” procedure.

Descendants-based. This variant “localizes” less than the point-based variant, but is incomparable with the order-based one. The idea is to keep those refinement atoms that were used for the parent constraint, and that are still weaker than the current conjunct that is to be approximated.

Finally, we state the soundness of our four exploration variants. The proof is by observing that $\mathtt {store}$ always represents, at the $i^{th}$ iteration of the loop of procedure “explore”, an over-approximation of the machine configurations obtained after i steps. Combined with Lemmas 2 and 3 and by well quasi ordering of $\sqsubseteq$ on the set of constraints for a finite number of refinement atoms.

Theorem 1

All four exploration variants are sound. In addition, each call to procedure “checkReachability” eventually terminates if only a finite number of calls to procedure “simulate” are executed.

Proof

Sketch. Let $\mathtt {work}_k$, $\mathtt {store}_k$ and $\mathtt {sleep}_k$ be the sets $\mathtt {work}$, $\mathtt {store}$ and $\mathtt {sleep}$ obtained at line 1 at the $k^{th}$ iteration of the loop in procedure “explore”. We can show the following propositions by induction on k (see the appendix for the details):

• (a) $[\![\mathtt {store}_k]\!]$ does not intersect $(q_{trgt}^{},\mathbb {c})$ for any valuation $\mathbb {c}$

• (b) $[\![\mathtt {store}_k]\!]$ intersects $(q_{init}^{},\mathbb {c})$ for every valuation $\mathbb {c}$

• (c) $[\![\mathtt {work}_k\cup \mathtt {sleep}_k]\!]$ is a subset of $[\![\mathtt {store}_k]\!]$

• (d) for each element $((\phi ,\psi ),\sigma _{}^{})$ of $\mathtt {store}_k$ such that $((\phi ,\psi ),\sigma _{}^{})\not \in \mathtt {work}_k$ and $\phi \in \texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(\mathtt {store}_k))$ and for each transition $\delta =(q_{}^{},gc,q'{}{})\in \varDelta$, the configurations in $\{(q'{}{},\mathbb {c}')|~\mathbb {c}'\in [\![{\texttt {post}}_{gc}(\texttt {clo}(\texttt {val}(\phi ),\texttt {box}(\phi )))]\!]\}$ are also in $[\![\mathtt {store}_k]\!]$

Soundness. Suppose the algorithm returns $\mathtt {unreachable}$. Then at some iteration, there is no element $((\phi ,\psi ),\sigma _{}^{})$ in $\mathtt {work}$ s.t. $\phi \in \texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(\mathtt {store}))$. Combined with propositions (b), (c) and (d), we have that $[\![\mathtt {store}]\!]$ is a fixpoint that is an overapproximation of all reachable configurations. Proposition (a) ensures that no element with state $q_{trgt}^{}$ exists in $\mathtt {store}$. If the algorithm returns a trace, then the test at line 4 ensures that $\texttt {st}(\phi _n)= q_{trgt}^{}$ for some $((\phi _n,\psi _n),\sigma _{}^{})$ and $\sigma _{}^{}=(\phi _0,\psi _0)\cdot \delta _{1}{}\cdots \delta _{n}{}\cdot (\phi _n,\psi _n)$ satisfies that $\texttt {st}(\phi _0)=q_{init}^{}$, $\texttt {st}(\phi _n)=q_{trgt}^{}$ and for $0\le i < n$, $(\texttt {st}(\phi _i),\texttt {val}(\phi _i))\xrightarrow []{\delta _{i+1}}(\texttt {st}(\phi _{i+1}),\texttt {val}(\phi _{i+1}))$. This because of the form of the added tuple at line 13 of “explore”.

Termination. The procedure “checkReachability” terminates if only a finite number of calls to procedure “simulate” are executed. This relies on the fact that the only source of non-termination can be the while loop in “explore” if the set $\texttt {cstrOf}(\mathtt {work})\cap \texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(\mathtt {store}))$ never becomes empty. Suppose there is an infinite sequence of constraints as $\phi _0 , \phi _1\ldots$ obtained in the while loop. First, we show that $i\ne j$ implies $\phi _i$ is not $\sqsubseteq$-equivalent with $\phi _j$ for any $i,j\ge 0$. This holds because an element is added to $\mathtt {store}$ only if there is no $\sqsubseteq$-equivalent element there (line 9 of “explore”). Even if an element is moved from $\mathtt {sleep}$ to $\mathtt {store}$ and $\mathtt {work}$ by “backtrack”, then it is done after removing the $\sqsubseteq$-equivalent element in $\mathtt {store}$ and $\mathtt {work}$. Second, we show that for any $0\le i < j$, $\phi _i \not \sqsubseteq \phi _j$. This holds because if $\phi _i \sqsubseteq \phi _j$, then $\phi _j$ could not be in $\texttt {min}_{\sqsubseteq }(\texttt {cstrOf}(\mathtt {store}))$ since $\phi _i$ (or an $\sqsubseteq$-equivalent constraint) is already there. Finally, since the number of calls to “backtrack” is finite, then the number of predicates being used in the boxes is also finite. Such a sequence would therefore violate Lemma 2. $\quad \square$

Fig. 3.

Comparing eager and lazy variants on a logarithmic scale.

7 Experimental Results

We have implemented our techniques in our open source tool Zaama. The tool and benchmarks are available online². The tool relies on the Z3 SMT solver [12] for its internal representations and operations.

The input of the prototype are counter machine encodings of boolean multi-threaded programs with broadcasts and arbitrary tests (as described in Sect. 3). We have experimented with more than eighty different counter machine reachability problems. These were obtained from our prototype tool Pacman [18] that checks local (i.e., assertion) or a global (e.g., deadlock freedom) properties in concurrent programs (some inspired from [11, 15]).

Given a property to check on a concurrent program, Pacman proceeds in predicate abstraction iterations. For each set of tracked predicates, it creates a counter machine reachability problem. Combining Pacman with Zaama results in a nested CEGAR loop: an outer loop for generating counter machine reachability problems, and an inner loop for checking the resulting problems. About 45 % of the generated counter machines are not monotonic. We tested all those machines separately with Zaama  in different settings for each benchmark and reported the execution times. Thus, the Pacman overhead is not included in the reported times. Note that although 55 % of the examples are monotonic, they still need refinement in forward exploration.

We also tested our benchmarks with the tool Breach introduced in [23]. Breach cannot take non-monotonic inputs and is inherently incapable of solving reachability problems for such systems which are the main target of this paper. Thus, we could apply it only to the monotonic benchmarks; for which, the runtime of Breach was less than 5 seconds in each. We consider this to be an encouraging result as we are working on adapting Breach to non-monotonic systems. The challenge is to have an under-approximation search engine for such systems and we are investigating possibilities to develop our own engine or to use acceleration tools such as FASTer [6].

We have chosen a time-out of 30 min for each of the variants: eager, point-based, order-based and descendants-based, both in forward and in backward. We have conducted our experiments on an Intel Core i7 2.93 GHz processor with 8GB of memory. We report on our results in Fig. 3 where we consider, for each setting, each lazy pair in addition to the pairs consisting in the eager and each lazy.

The forward explorations turned out to be faster than the corresponding backward ones in about 25 % of the examples. We expected the forward exploration to be slower as it needs several refinement steps because it starts from the initial configurations which are typically much more constrained than the target configurations. We considered the forward exploration because it offers more possibilities to test the effect of localizing the refinement in problems that typically require more refinement steps in forward. Indeed, the figures show that the times of the different variants coincide more often in backward than in forward, and overall, there has been many more time-outs in forward than in backward.

Furthermore, the lazy variants were able to conclude on most of the reachability problems, in fact each of the reachability problems has been solved by at least one of the lazy variants (except for one problem in backward), when the eager variant timed out on several of them. This is an encouraging result that confirms the advantages of localizing refinement. There are some cases where the eager variant did better than all lazy ones. These correspond to cases where localization required more refinement efforts to reach a conclusion.

We also observe that the order-based approach times out in about half the forward seraches, while the point-based only times out in two cases. This goes against the initial intuition that larger valuations would profit from the refinement predicates of the smaller ones. One explanation could be that if the larger valuation would require the same predicate as the smaller one, then adding the predicate would result in a redundant representation that should be eliminated. It therefore seems that it does not take long for the point-based to discover this redundancy while still profiting from the localization of the refinement. Instead, the order-based uses predicates even when they are not proven to be needed resulting in finer grained symbolic elements that slow down the exploration.

It is interesting to observe that the descendants-based approach did better in forward than the point-based approach. One explanation could be that, in forward, relevant refinement interpolants sometimes correspond to weak inductive invariants that get propagated by this approach. In backwards it seems, at least for our examples, that the invariants corresponding to the “bad” configurations do not profit from this parent-child transmission.

8 Conclusion

We have introduced and discussed three different ways of localizing constrained monotonic abstraction in systems with infinite control. For this, we have targeted reachability problems for (possibly non-well structured) counter machines obtained as abstractions of concurrent programs. Our new techniques allow us to avoid systematically trashing the state space explored before encountering the false positives that necessitate the introduction of new refinement predicates. This allowed us to consistently improve on the existing eager exploration, both in forward and in backward explorations. Possible future works concern combining forward and backward approximations, using the pivot configuration to make possible the choice of interpolants that are easier to generalize and assessing the feasibility of combination with new partial order techniques.