Incompleteness, Counterexamples and Refinements in Abstract Model-Checking

Roberto Giacobazzi^{1} and Elisa Quintarelli^{1}^{,}^{2}

1 Dip. di Informatica, Università di Verona. Strada Le Grazie 15, 37134 Verona (Italy). 2 Dip. di Elettronica e Informazione, Politecnico di Milano. Piazza Leonardo da Vinci, 20133 Milano (Italy). E-mail: giaco|quintare@sci.univr.it

Abstract. In this paper we study the relation between the lack of completeness in abstract interpretation of model-checking and the structure of the counterexamples produced by a model-checker. We consider two dual forms of completeness of an abstract interpretation: Forward and backward completeness. They correspond respectively to the standard γ/α completeness of an abstract interpretation and can be related with each other by adjunction. We give a constructive characterization of Clarke et al.’s spurious counterexamples in terms of both forward and backward completeness of the underlying abstract interpretation. This result allows us to understand the structure of the counterexamples that can be removed by systematically refining abstract domains to achieve completeness with respect to a given operation. We apply our result to improve static program analysis by refining the model-checking of an abstract interpretation.

Keywords: Completeness, Model-checking, Verification, Abstract Interpretation, Domain Refinement, Program Analysis.

1 Introduction

Many authors recognized in the possibility of modifying abstract models by modifying abstractions a great potential for improving abstract model-checking in precision and reducing complexity (e.g. see Section 9 in [10]), but few applications of these techniques are known in the field of model-checking. In this paper we observe that there exists a strong connection between the standard notion of complete abstract interpretation [6, 7, 14] and the corresponding one for abstract model-checking [10, 2], and we show how the latter one can be achieved by minimally modifying abstract domains.

Completeness in abstract interpretation corresponds to require that no loss of precision is introduced by approximating a semantic function computed on abstract objects with respect to approximating the same computation on concrete objects. Therefore, no loss of precision is accumulated in abstract computations by approximating concrete input objects. This property comes directly from the original definition of Galois-connection based abstract interpretations [6, 7]: If α and γ is a pair of adjoint functions in a Galois connection specifying an abstract interpretation, and 𝒪 and 𝒪^{♯} are respectively the concrete and abstract operations, we say that the abstract interpretation is complete if α∘𝒪 = 𝒪^{♯}∘α. Recently, Giacobazzi et al. [14] observed that completeness for an abstract interpretation, i.e., abstract domains and abstract operations, only depends upon the structure of the underlying abstract domains and, in particular, that it is always possible to make any abstract domain A complete with respect to a concrete function 𝒪 by minimally extending or even reducing A. This process is known as the complete shell/core of A. This means that a systematic domain transformer can be introduced to improve precision of domains with respect to a given function by letting the new domains be complete with respect to this function.

The problem

The idea of abstract (state-)model-checking is that of verifying temporal properties against an approximated model which is systematically derived from the concrete semantics of the system we want to analyze. This is always achieved by approximating the information contained in its states. Since the pioneering work on model-checking and abstraction by Clarke et al. [3], a number of works have applied this idea to reduce the phenomenon of “state explosion” (e.g. [8, 10, 17]). Indeed, verifying a temporal logic formula against a model is in general a hard problem (PSPACE complete for CTL*) [1, 11, 16]. The problem of refining abstract model checking is precisely that of improving precision in temporal logic verification by refining a state partition (called in [3] an abstraction) that turns out to provide a too rough abstract model for verifying a given temporal property of interest. Roughly speaking, by refining the abstraction in abstract model-checking we gain precision, namely the refined model becomes more selective (being closer to the concrete model) than the abstract one. Moreover, the size of the new refined abstract model has to be kept as small as possible in order to avoid to re-introduce the “state explosion” phenomenon. Formulated in this way, this is indeed precisely a domain refinement problem: Improve abstractions (viz. enhance domains) in such a way that the new abstraction contains the least amount of information that is needed to achieve a given precision degree [12, 13]. It is not an easy task to apply the standard abstract domain refinement theory ([7, 12, 13]) to abstract model-checking refinement. This because of two reasons:

(1) Even though any state partition can be associated with a Galois connection, the reverse does not hold in general. Therefore it is not always immediate to associate a refined state partition with a refined abstract domain (or equivalently Galois connection) as the latter may not correspond to a state partition. (2) We need to express the meaning of improving precision in abstract model-checking by refining domains. This has to be related with the structure of the formulas that are verified in the new refined model. We solve both these problems in the context of abstract domain refinements to achieve complete abstract model checking.

Main results

In abstract model-checking soundness means that when a property is true in the abstract model it will also be true in the concrete one. However, the approximation may not be complete in the sense of model-checking, i.e., if the property of interest is false in the abstract model, the counterexample produced by the model-checker may be the result of some particular traces in the approximated model, which are not present in the concrete one, i.e., which do not correspond to any concrete computation. In [2] this phenomenon has been isolated, and these counterexamples have been called spurious. We consider spurious counterexamples as a measure for the achieved precision in systematically refining abstract model-checking by standard domain transformers. We first introduce the notions of backward and forward completeness for an abstract interpretation. While backward completeness corresponds precisely to the standard notion of completeness for an abstract interpretation [7, 14], forward completeness is less well-known and it corresponds to what is sometimes called “exactness” of an abstract interpretation (e.g. [4]). We show that forward and backward completeness are dual notions, and that, as well as for backward completeness, also forward completeness can be achieved by minimally refining abstract domains. Then we observe that any abstract domain refinement induces a refined state partition which in turn reduces the amount of spurious counterexamples in the refined abstract model. Finally we show that the counterexample-guided abstraction refinement by Clarke et al. [2] corresponds precisely to iteratively compute the backward (forward)-complete shell of the corresponding abstraction with respect to the forward (backward) state transition function. This provides a purely algebraic characterization of spurious counterexamples in terms of standard abstract interpretation theory. Moreover, this result allows us to characterize the structure of spurious counterexamples that can be removed by refining a domain to achieve completeness with respect to an arbitrary function, therefore including most domain refinements known in the literature. Our results are applied in the systematic refinement of data-flow analysis as the model-checking of abstract interpretations, as formulated in [20].

Related works

The body of research on the connection among model-checking, abstract interpretation and data-flow analysis is huge, even though this field still represents a major challenge in formal methods. In particular the problem of completeness in abstract model-checking has been studied by a number of authors both theoretically and from the point of view of improving model-checking algorithms. In [2] the authors proposed an automatic refinement technique which uses information obtained from erroneous counterexamples produced by a model-checker. They introduced the notion of spurious counterexample and gave an algorithm based on the inverse image of the forward transition function to refine the abstraction. However, the authors did not consider the classical notions of abstract interpretation in order to improve the precision of the approximated models.

In our work we prove that this algorithm can be formulated as an instance of the more general problem of making an abstraction complete in the standard sense of abstract interpretation. In [9] Cousot and Cousot introduced a novel general temporal language, inspired by Kozen’s μ-calculus, which includes most standard specification languages such as CTL and CTL* as special cases. The authors proved that the classical state-based model-checking of this language is an abstract interpretation of its trace-based semantics, which turns out to be incomplete. More recently Ranzato [19] found the complete shell according to [14] of Cousot’s state-based model-checking abstraction. This construction has been applied to the whole specification language introduced in [9], proving that there exists no complete abstraction which includes the state-model-checking and it is strictly more abstract than the trace-based model-checking. This proves that it is impossible for state-model-checking to achieve completeness with respect to trace-model-checking, without including the traces them self. In [5] the authors introduced a new concept of completeness, called partial completeness, for problems which are intended to check abstract fix-points for specifications. A checking algorithm is partially complete when in case of termination the answer is exact. This notion can be directly applied in model-checking problems, where one is interested in partially complete abstractions, i.e., approximations of a given model which always yield an affirmative answer when the specification is correct (i.e. it holds in the original model) and the algorithm does terminate. This notion of completeness seems different from the one considered in this paper, but further research is needed to better understand the relation between these two notions of completeness.

Structure of the paper

The paper is organized as follows: In Sections 2 and 3 we recall first the main notions concerning temporal logic and model checking, and then the standard theory of Galois-connection based abstract interpretation. The main results of the paper are in Section 4, Section 5, and Section 6. In Section 4 we introduce forward and backward completeness of an abstract interpretation and we study the relation between these two notions and a constructive method to minimally modify domains in order to achieve either forward or backward completeness. In Section 5 we introduce abstract model checking refinement by domain transformers and in Section 6 we characterize the precision of a refined abstract model in terms of Clarke’s spurious counterexamples. Finally, in Section 7 we give a model-checking perspective of the problem of complete data-flow analysis. Section 8 concludes with future works.

2 Temporal logic and model-checking

In the following we consider a fragment ∀CTL* of the branching time temporal logic CTL* [3, 11]: The formulas of ∀CTL* do not contain existential quantifiers. Of course, all the results apply to the universal fragment of the weaker language CTL, as well. In ∀CTL* universal properties are expressed through the path quantifier ∀ (“for all futures”) that quantifies over (infinite) execution sequences. The temporal operators G (Generally, always), F (Finally, sometime) X (neXt time), and U (Until) express properties of a single execution sequence. These operators, as well as other syntactic possibilities, can be freely nested in a formula. Given a set P rop of propositions, the set Lit of literals is defined as Lit = P rop∪{¬q | q ∈ P rop}∪{true, false}. State formulas ϕ and Path formulas ψ are inductively defined by the following grammar, where p ∈ Lit:

State formulas: ϕ ::= p | ϕ ∧ ϕ | ϕ ∨ ϕ | ∀ψ
Path formulas: ψ ::= ϕ | ψ ∧ ψ | ψ ∨ ψ | Gψ | F ψ | Xψ | U(ψ, ψ)

Observe that negation is allowed only for literals. Therefore, the results that allow us to write the existential modal operator using universal formulas do not hold here. Observe also that F is superfluous because F ψ = U(true, ψ) . A transition system is a pair ⟨Σ, R⟩ consisting of a set Σ of states and a transition relation R ⊆ Σ × Σ that is assumed to be total. A Kripke structure is a tuple 𝕄 = ⟨Σ, R, I, ∥ · ∥⟩ where ⟨Σ, R⟩ is a transition system, I ⊆ Σ is the set of initial states, and ∥ · ∥: Lit ⟶ ℘(Σ) is the interpretation function such that ∥ p ∥= { s ∈ Σ | s ⊧ p }. For ∀CTL^{∗} the notion of satisfaction of a state formula ϕ by a state s (s ⊧ ϕ) is as usual [10]. If 𝕄 = ⟨Σ, R, I, ∥ ∘ ∥⟩ is a Kripke structure, we say that 𝕄 ⊧ φ if and only if ∀s ∈ I : s ⊧ φ. Given a temporal formula φ the satisfiability problem for φ is that of checking if there exists a Kripke structure 𝕄 such that 𝕄 ⊧ φ. In the case of CTL* (hence of ∀CTL^{∗}) this problem is decidable [11]. For verification purposes the following problem is known as the (global) model-checking problem (MCP): given 𝕄 = ⟨Σ, R, I, ∥ ∘ ∥⟩ and a formula φ, check if 𝕄 ⊧ φ.

3 Abstract Interpretation

In the following ⟨C, ≤, ∨, ∧, ⊤, ⊥⟩ denotes a complete lattice C, with ordering ≤, lub ∨, glb ∧, greatest element (top) ⊤, and least element (bottom) ⊥. The downward closure of S ⊆ C is defined as ↓S =^{def} {x ∈ C | ∃y ∈ S. x ≤ y}. ↓ x is a shorthand for ↓ {x}, while the upward closure ↑ is dually defined. The notation C ≅ D denotes that C and D are isomorphic possibly ordered structures. Recall that a function f ∈ C → D is (Scott-)continuous if f preserves lub’s of (nonempty) chains iff f preserves lub’s of directed subsets. In the following we consider Galois connection based abstract interpretation [6]. A pair of functions f : A → B and g : B → A forms an adjunction if

∀x ∈ A.∀y ∈ B. f(x) ≤_{B} y ⇔ x ≤_{A} g(y).

f (resp. g) is the left- (right-)adjoint to g (f) and it is an additive (co-additive) function, i.e., f preserves lub’s (glb’s) of all subsets of A (empty-set included). Additive and co-additive functions f admit respectively right and left adjoint:

f^{+} =^{def} λx. ⋁ { y | f(y) ≤ x } and f^{−} =^{def} λx. ⋀ { y | x ≤ f(y) } respectively.

Remember that (f^{+})^{−} = (f^{−})^{+} = f. A Galois connection (GC for short) is an adjunction between posets, and it is denoted (A, f, B, f^{+}). In GC-based abstract interpretation the concrete and abstract domains, C and A, are often assumed to be complete lattices and are related by abstraction α : C → A and concretization γ : A → C maps forming a GC (C, α, A, γ). If in addition ∀a ∈ A. α(γ(a)) = a, then we call (C, α, A, γ) a Galois insertion (GI) of A in C. When (C, α, A, γ) is a GI then each value of the abstract domain A is useful in representing C, because all the elements of A represent distinct members of C, being γ 1-1. Any GC may be lifted to a GI by identifying in an equivalence class those values of the abstract domain with the same concretization. This process is known as reduction of the abstract domain. An upper closure operator on a poset C is an operator ρ : C → C which is monotone, idempotent, and extensive (∀x ∈ C. x ≤ ρ(x)). Lower closures are dually defined. The set of all upper (lower) closure operators on C is denoted by uco(C) (lco(C)). Each closure is uniquely determined by the set of its fix-points ρ(C). A fundamental property of closure operators is that if C is a complete lattice then both ⟨uco(C), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ ordered pointwise, and ⟨ρ(C), ≤, ∨_{ρ}, ∧, ⊤, ρ(⊥)⟩ with ∨_{ρ}X = ρ(∨X), are complete lattices. It is well known since [7] that abstract domains can be equivalently specified either as Galois insertions or as (sets of fix-points of) upper closures on the concrete domain. In particular X ⊆ C is the set of fix-points of an upper closure ρ on C iff X is a Moore-family of C, i.e., X = ℳ(X) =^{def} {∧S | S ⊆ X} — where ∧∅ = ⊤ ∈ ℳ(X), iff X is isomorphic to an abstract domain A in a GI (C, α, A, γ), i.e. A ≅ ρ(C) with ι : ρ(C) → A and ι^{−1} : A → ρ(C) being the isomorphism, and (C, ι∘ρ, A, ι^{−1}) is the GI, i.e. ρ = γ∘α. Therefore uco(C) is isomorphic to the so called lattice of abstract interpretations of C [7]. For any X ⊆ C, ℳ(X) is called the Moore-closure of X in C, i.e., ℳ(X) is the least (w.r.t. set-inclusion) subset of C which contains X and it is a Moore-family of C. In this case A ⊑ B iff B ⊆ A as Moore families of C, iff A is more concrete than B. In the following we will find particularly convenient to identify closure operators (and therefore abstract domains) with their sets of fix-points, possibly by using as notation capital Latin letters.

4 Backward and forward completeness

In abstract interpretation there are two equivalent ways to express the soundness of an abstraction [6]. Let C be a complete lattice, f : C → C, (C, α, A, γ) be a Galois insertion, and f^{♯} : A → A. Then (C, α, A, γ) and f^{♯} provide a sound abstraction of f if α∘f ≤ f^{♯}∘α, or equivalently (by adjunction) if f∘γ ≤ γ∘f^{♯}. While these two definitions of soundness are equivalent, they are not equivalent when equality is required. In the first case α∘f = f^{♯}∘α means that no loss of precision is accumulated by approximating the input arguments of a given semantic function; while f∘γ = γ∘f^{♯} means that no loss of precision is accumulated by approximating the result of computations on abstract objects. These two notions represent therefore two different forms of completeness: The first is related with input arguments of a computation, while the second is related with its output.

We distinguish here between these two forms of completeness: The first is called backward (ℬ) and the second is called forward (ℱ) completeness. The reason for these names will be clear later in the paper.

Definition 1. Let C be a complete lattice, f : C → C, (C, α, A, γ) be a Galois insertion, and f^{♯} : A → A.

– (C, α, A, γ) and f^{♯} are ℬ-complete for f if α∘f = f^{♯}∘α.

– (C, α, A, γ) and f^{♯} are ℱ-complete for f if f∘γ = γ∘f^{♯}.

ℬ-completeness (see [14]) corresponds to ask that the approximate function f^{♯} perfectly mimics the concrete function f, when the latter is approximated in A, viz. both are compared in the abstract domain A. Conversely, ℱ-completeness corresponds to ask that f^{♯} perfectly mimics the function f applied to the same abstract arguments, viz. they are both compared in the concrete domain C. The following proposition extends a result in [14] about ℬ-completeness to ℱcompleteness. In this case there exists an either ℬ or ℱ complete abstract function f^{♯} in an abstract domain A iff the best correct approximation α∘f∘γ of f is respectively either ℬ or ℱ complete. This means that, as well as for ℬcompleteness [14], also ℱ-completeness is a property of abstract domains, namely a property of the GI (C, α, A, γ).

Proposition 1. Let C be a complete lattice, f : C → C, and (C, α, A, γ) be a Galois insertion. There exists f^{♯} : A → A such that (C, α, A, γ) and f^{♯} are ℬ-complete (ℱ-complete) for f iff α∘f = α∘f∘γ∘α (f∘γ = γ∘α∘f∘γ).

Therefore, we can define when a domain (closure operator) is ℬ/ℱ-complete for a semantic function as follows.

Definition 2. Let C be a complete lattice and ρ ∈ uco(C) be an abstract domain. ρ is ℬ(ℱ)-complete for f if ρ∘f = ρ∘f∘ρ (f∘ρ = ρ∘f∘ρ).

While ℬ-completeness is well known in abstract interpretation and it corresponds to the standard notion of completeness [18, 14], the notion of forward completeness is less known. ℬ-completeness means that the domain ρ is expressive enough such that no loss of precision is accumulated by abstracting in ρ the arguments of a function f. Conversely, ℱ-completeness means that no loss of precision is accumulated by approximating the result of the function f computed in ρ. This justifies the choice of the backward and forward names above. In the following

we denote by ℱ(C, f) =^{def} { ρ | f∘ρ = ρ∘f∘ρ } and ℬ(C, f) =^{def} { ρ | ρ∘f = ρ∘f∘ρ }

respectively the set of ℱ and ℬ complete abstractions of C for f. It is worth noting that in general ℱ(C, f) ⊈ ℬ(C, f) and ℱ(C, f) ⊈ ℬ(C, f), namely they are incomparable notions.

Example 1. Let Sign^{+} be the domain in Fig. 1 which is an abstraction of ⟨℘(ℤ), ⊆⟩ for the analysis of integer variables and sq : ℘(ℤ) → ℘(ℤ) be the square operation defined as follows: sq(X) = { x^{2} | x ∈ X } for X ∈ ℘(ℤ). Let ρ ∈ uco(℘(ℤ)) be the closure operator associated with Sign^{+}, i.e. ρ = γ∘α, where the abstraction and concretization maps are the most obvious ones. The best correct approximation of sq in Sign^{+} is sq^{♯} : Sign^{+} → Sign^{+} such that sq^{♯}(X) = ρ(sq(X)), with X ∈ Sign^{+}. It is easy to see that the upper-closure operators ρ_{a} = {ℤ, [0, +∞], [0, 10]} and ρ_{b} = {ℤ, [0, 2], [0]}, respect the following facts: ρ_{a} = {ℤ, [0, +∞], [0, 10]} ∈ ℱ(Sign^{+}, sq^{♯}) but ρ_{a} = {ℤ, [0, +∞], [0, 10]} ∉ ℬ(Sign^{+}, sq^{♯}) (for example, ρ_{a}(sq^{♯}(ρ_{a}([0]))) = [0, +∞] but ρ_{a}(sq^{♯}([0])) = [0, 10]) and ρ_{b} = {ℤ, [0, 2], [0]} ∈ ℬ(Sign^{+}, sq^{♯}) but ρ_{b} = {ℤ, [0, 2], [0]} ∉ ℱ(Sign^{+}, sq^{♯}) (e.g. ρ_{b}(sq^{♯}(ρ_{b}([0, 2]))) = ℤ but sq^{♯}(ρ_{b}([0, 2])) = [0, 10]). The arrows in Fig. 1 show the non fix-points results of sq^{♯}.

\begin{matrix}[figure: •; •; •; •; •; •; ℤ; [0, +∞]; [0, 10]; [0, 2]; [0]; [−∞, 0]] & [figure: •; •; •; ∘; ∘; ∘; ℤ; [0, +∞]; [0, 10]; [0, 2]; [0]; [−∞, 0]] & [figure: •; ∘; ∘; •; •; ∘; ℤ; [0, +∞]; [0, 10]; [0, 2]; [0]; [−∞, 0]] \\ Sign^{+} & (a) & (b) \end{matrix}

Fig. 1. The abstract domain Sign^{+} and two abstractions

Clearly, when an abstract domain ρ is both ℬ and ℱ complete for f, then ρ is a morphism, i.e., ρ∘f = f∘ρ, namely ℱ(C, f) ∩ ℬ(C, f) = { ρ | ρ∘f = f∘ρ }. Note that in the Example 1, {ℤ, [0, +∞], [−∞, 0], [0]} ∈ ℱ(Sign^{♯}, sq^{♯}) ∩ ℬ(Sign^{♯}, sq^{♯}).

The following result is the main result in [14] and it is the basis for a constructive characterization of the complete shell of an abstract domain, viz. the least (most abstract) domain which is ℬ-complete and includes a given domain. This result constructively characterizes the structure of ℬ-complete abstract domains for continuous functions. Recall that, if f : C → C is a unary function, then f^{−1}(y) = { x | f(x) = y }.

Theorem 1 ([14]). Let f : C → C be continuous and ρ ∈ uco(C). Then ρ is ℬ-complete for f iff ⋃_{y∈ρ(C)} max(f^{−1}(↓ y)) ⊆ ρ(C).

It is easy to see in Example 1 that ρ_{a} is not ℬ-complete because it does not include the maximal inverse image of sq^{♯} (see Fig. 1), namely the point [0, 2].

An analogous, but simpler to prove, result can be stated for ℱ-completeness. In this case, we can characterize ℱ-complete domains for merely monotone operators.

Theorem 2. Let f : C → C be monotone and ρ ∈ uco(C). ρ is ℱ-complete for f iff ∀x ∈ ρ(C). f(x) ∈ ρ(C).

Therefore, while ℬ-complete domains are closed under (maximal) inverse image of the function f, ℱ-complete domains are closed under direct image of f. It is easy to see in Example 1 that ρ_{b} is not ℱ-complete because it does not include the direct image of sq^{♯} (see Fig. 1), namely the points [0, 10] and [0, +∞]. Both Theorem 1 and 2 together specify a strong relation between ℬ and ℱ completeness, which can be specified in terms of adjunction when f admits a right adjoint f^{+}.

Corollary 1. Let C be a complete lattice and f : C → C be an additive function. Then ℬ(℘(S), f) = ℱ(℘(S), f^{+}).

Moreover it is always possible, in view of Theorem 1 and 2, to associate with each continuous semantic function f : C → C a corresponding domain refinement that transforms any abstract domain A into the closest (most abstract) ℬ/ℱcomplete domain for f which includes (is more concrete than) A. In the first case we obtain the (ℬ-)complete shell in [14], while in the second we obtain what we call the ℱ-complete shell.

Definition 3. Let C be a complete lattice and f : C → C be a continuous function. We define ℛ_{f}^{ℬ} : uco(C) → uco(C) and ℛ_{f}^{ℱ} : uco(C) → uco(C) such that:

– ℛ_{f}^{ℬ} = λX ∈ uco(C). ℳ(⋃_{y∈X} max(f^{−1}(↓ y)));

– ℛ_{f}^{ℱ} = λX ∈ uco(C). ℳ(f(X)).

It is immediate to prove that both ℛ_{f}^{ℬ} and ℛ_{f}^{ℱ} are monotone operators on uco(C). The following result, which follows by Theorem 1 and 2, characterizes in a unique domain-equational form the ℬ/ℱ-complete shell of abstract domains for a continuous function f : C → C.

Theorem 3. Let f : C → C be a continuous function and A ∈ uco(C) be an abstract domain. Let ℓ ∈ {ℬ, ℱ}:

X is ℓ-complete for f and X ⊑ A iff X = A ⊓ ℛ_{f}^{ℓ}(X);

Therefore, the greatest (viz, most abstract) domain which includes A and which is ℓ-complete for f is 𝒮_{f}^{ℓ}(A) = gfp(λX. A ⊓ ℛ_{f}^{ℓ}(X)). This domain is called the ℓ-complete shell of A with respect to f. Note that, as proved for the ℬcomplete shell in [14], ℛ_{f}^{ℓ} above is a co-additive operator on the lattice of abstract interpretations uco(C), and that λX. 𝒮_{f}^{ℓ}(X) is a monotone, idempotent, and reductive operator on uco(C), i.e. 𝒮_{f}^{ℓ} ∈ lco(uco(C)).

5 Refining state partitions vs refining domains

In this section we study how to systematically refine abstract model-checking, namely we consider functions of type ℘(Σ) → ℘(Σ) with Σ being the set of states in a transition system ⟨Σ, R⟩. The following definition introduces the notion of abstract Kripke structure according to Dams et al. [10].

Definition 4. Let 𝕄 = ⟨Σ, I, R, ∥ ∘ ∥⟩ be a Kripke Structure and (℘(Σ), α, A, γ) be a GI. The corresponding abstract Kripke Structure 𝕄^{♯} = ⟨A, I^{♯}, R^{♯}, ∥ ∘ ∥^{♯}⟩ is defined as follows:

– a ∈ I^{♯} iff ∃d ∈ I. α({d}) = a;

– R^{∃∃} =^{def} { (X, Y) | ∃_{x∈X}∃_{y∈Y} . R(x, y) };

– R^{♯}(a_{1}, a_{2}) iff a_{2} ∈ { α(Y) | Y ∈ min { Y′ | R^{∃∃}(γ(a_{1}), Y′) } };

– ∥ p ∥^{♯}=^{def} { a ∈ A | γ(a) ⊆∥ p ∥ }.

Note that for any a ∈ A, the minimal sets Y′ such that R^{∃∃}(γ(a), Y′) are all singletons.

In the following we consider abstract domains as specified by a GI, or equivalently by a closure operator on ℘(Σ), where Σ is the set of states of a transition system ⟨Σ, R⟩. This is apparently in contrast with the original (standard) definition of abstract model-checking by Clarke et al. [3]. In this latter case the abstraction is specified by a surjection function, called state partition, h : Σ → S on a given set S of abstract states. Notice that any surjection h : Σ → S induces an equivalence relation ≡ on the set of states Σ in the following way: Let a, b ∈ Σ, then a ≡ b iff h(a) = h(b). Given a surjection h : Σ → S we can immediately derive a GI in the following way: (℘(Σ), α_{h}, ℘(S), γ_{h}), where α_{h}(X) =^{def} { h(x) | x ∈ X } is the abstraction function and γ_{h}(Y) =^{def} { x | h(x) ∈ Y } is the concretization function. Note that the GI is defined by considering ℘(S) instead of S, because it is not assumed that the set of abstract states S is partial ordered.

The main problem with this approach and abstract domain refinement is that, in general, if f : ℘(Σ) → ℘(Σ) is some predicate transformer on the transition system ⟨Σ, R⟩, then the refined domain 𝒮_{f}^{ℓ}(γ_{h}∘α_{h}) ∈ uco(℘(Σ)), with ℓ ∈ {ℱ, ℬ}, may not be of the form ℘(S) for some set of abstract states S. In particular 𝒮_{f}^{ℓ}(γ_{h}∘α_{h}) may not be a Boolean algebra, and therefore the powerset of some set. Because we abstract state-model-checking, it is sufficient to observe how the refined domain abstracts each single state. Indeed, any abstract domain refinement induces a domain surjection in the following way: Let

Ŝ ≅ {𝒮_{f}^{ℓ}(γ_{h}∘α_{h})({x}) | x ∈ Σ}, then the function ĥ =^{def} λx ∈ Σ. 𝒮_{f}^{ℓ}(γ_{h}∘α_{h})({x})

is a surjection from Σ into Ŝ such that: |S| ≤ |Ŝ| and (℘(Σ), αĥ, ℘(Ŝ), γĥ) is a GI. This corresponds to improve the partition induced by h into a finer partition of the concrete states as induced by ĥ. This improvement is obtained by considering a new set of abstract states each one consisting of the (unique) best possible abstraction of each concrete state according to the refined closure 𝒮_{f}^{ℓ}(γ_{h}∘α_{h}).

Proposition 2. Let h : Σ → S be a state partition and (℘(Σ), α_{h}, ℘(S), γ_{h}) be the corresponding GI. If 𝒮 : uco(℘(Σ)) → uco(℘(Σ)) is a domain refinement, i.e. a monotone function such that ∀X ∈ uco(℘(Σ)). 𝒮(X) ⊑ X, then the function h_{𝒮} : Σ → {𝒮(γ_{h}∘α_{h})({x}) | x ∈ Σ} such that h_{𝒮} = λx. 𝒮(γ_{h}∘α_{h})({x}) is a refinement of the state partition h.

Therefore, the standard theory of abstract domain refinement (see [13]) can be fully applied directly to refine any abstract (state-)model-checking problem. In this latter case, a refined state partition function can be systematically derived from the refined abstract domain as described in Proposition 2.

Example 2. Consider the transition system ⟨[0, 9], R⟩ where the transition relation R is shown on the left in Fig. 2 with continuous lines. Consider the state partition function h(x) = x mod 4. Following Definition 4, this induces an abstract Kripke structure associated with the GI (℘([0, 9]), α_{h}, ℘({a, b, c, d}), γ_{h}) as depicted in Fig. 2 with empty boxes and dashed lines. Let f : ℘([0, 9]) → ℘([0, 9]) be such that f(X) = {3}. The forward complete shell of γ_{h}∘α_{h} is gfp(λX. γ_{h}∘α_{h} ⊓ ℛ_{f}^{ℱ} (X)) = ℛ_{f}^{ℱ} (γ_{h}∘α_{h}), and it is immediate to observe that it induces a new state partition function ĥ such that

ĥ(x) = \{ \begin{matrix}x & if x = 3, 7 \\ h(x) & otherwise \end{matrix}

The GI (℘([0, 9]), α_{h}, ℘({a, b, c, d}), γ_{h}) is not ℱ-complete for f, e.g. if ρ_{h} = γ_{h}∘α_{h} then f(ρ_{h}({2, 6})) = {3} but ρ_{h}(f(ρ_{h}({2, 6}))) = {3, 7}. In this case, in order to obtain the complete shell of ρ_{h} we have to add the abstract state {3} to the abstract domain. This leads to a partition of the abstract state {3, 7} into two more concrete states: {3} which is introduced by adding the forward image of f, and {7} which is a new state (actually, it is a renaming of the state {3, 7}) corresponding to the (unique) best possible approximation in ℛ_{f}^{ℱ} (γ_{h}∘α_{h}) of the concrete state 7. This induces a refined abstract Kripke structure associated with the refined GI (℘([0, 9]), αĥ, ℘({a, b, c, d, e}), γĥ), as shown on the right in Fig. 2.

[figure: •; •; •; •; •; •; •; •; •; •; □; □; □; □; 1; 5; 9; 2; 6; 3; 7; 0; 4; 8; a; b; c; d; •; •; •; •; •; •; •; •; •; •; □; □; □; □; □; 1; 5; 9; 2; 6; 3; 7; 0; 4; 8; a; b; e; c; d]

Fig. 2. An abstract Kripke structure and its refinement

6 Completeness and counterexamples

We are in the position to apply forward or backward completeness abstract domain refinement to abstract (state-)model-checking problems. In this section we relate the abstract domain refinement for both backward and forward completeness with the presence of suitable counterexamples in abstract model-checking.

A path in a Kripke Structure 𝕄 = ⟨Σ, I, R, ∥ ∘ ∥⟩ is an infinite sequence in ℕ → Σ, denoted π = s_{0}, s_{1}, …, such that s_{0} ∈ I and for every i ∈ ℕ, R(s_{i}, s_{i+1}) holds. Traditionally, a terminating execution has a final state which is repeated forever. With π_{i} we denote i-th state in the path, i.e., s_{i}. Given a Galois insertion (℘(Σ), α, A, γ) and concrete and abstract paths π and π^{♯} respectively, we denote by α(π) the sequence α(π_{0}), α(π_{1}), … and by γ(π^{♯}) the set { π | α(π) = π^{♯} }. Given a path π and a state x ∈ Σ, x ∈ π iff ∃i ∈ ℕ such that x = π_{i}. The forward predicate transformer associated with R is post[R] : ℘(Σ) → ℘(Σ), which is defined as post[R](X) = { s ∈ Σ | R(x, s) ∧ x ∈ X }. Dually, we can define the backward predicate transformer associated with R as p̃re[R] : ℘(Σ) → ℘(Σ), which is defined as p̃re[R](X) = { s ∈ Σ | ∀x ∈ Σ. R(s, x) ⇒ x ∈ X }. The following is a well known fact about forward and backward predicate transformers (e.g. [15]).

Proposition 3. (℘(Σ), post[R], ℘(Σ), p̃re[R]) is a Galois connection.

Let us consider a domain refinement which is specified as the ℱ/ℬ-complete shell with respect to a continuous function f : ℘(Σ) → ℘(Σ) as given in Theorem 1. Let R_{f} ⊆ Σ ×Σ be the relation associated with f, i.e. such that R_{f}(x, y) ⇔ y ∈ f({x}). It is immediate to observe that f = post[R_{f}].

Proposition 4. Let f : ℘(Σ) → ℘(Σ) be additive. Then we have

ℬ(℘(Σ), f) = ℬ(℘(Σ), post[R_{f}]) = ℱ(℘(Σ), f^{+}) = ℱ(℘(Σ), p̃re[R_{f}]).

Traditionally, a model-checker is used to determine whether a temporal formula holds in a model. If the answer is negative, i.e., the model does not possess the property specified by the formula, then the model checker generates a counterexample. Let 𝒮 : uco(C) → uco(C) be an abstract domain refinement, i.e., a monotone operator such that 𝒮(X) ⊑ X for any abstract domain X ∈ uco(C) [13]. It is immediate to observe that 𝒮 reduces the number of counterexamples that might be generated by the model-checker. Recall that, given a Kripke structure 𝕄 = ⟨Σ, I, R, ∥ ∘ ∥⟩ and a formula φ ∈ ∀CTL*, 𝕄 |̸= φ iff ∃s ∈ I. s |̸= φ, iff there exists a path starting at I which does not satisfy φ. This because ∀CTL* can only express formulas that describe behaviors that should hold on all paths from the initial states. Hence, if A is an abstract domain and 𝕄^{A} and 𝕄^{𝒮(A)} are respectively the abstract and refined Kripke structures associated with A and 𝒮(A), then we have that:

{ φ | 𝕄^{A} |̸= φ } ⊇ { φ | 𝕄^{𝒮(A)} |̸= φ } .

It is therefore natural to consider counterexamples as a measure of the achieved precision in abstract model-checking when the abstract domain is refined. However, not all counterexamples are admissible, because an abstract counterexample might not be valid in the concrete model. Clarke’s et al. [2] introduced the notion of spurious counterexample in order to model this situation^{1}.

1 Note that we consider path counterexamples only. Clarke’s et al. [2] consider instead loop counterexamples, which reduce to paths by means of loop unfolding.

Definition 5. Let (℘(Σ), α, S^{♯}, γ) be a GI. Consider the concrete and abstract Kripke structures ⟨Σ, I, R, ∥ ∘ ∥⟩ and ⟨S^{♯}, I^{♯}, R^{♯}, ∥ ∘ ∥^{♯}⟩ and φ ∈ ∀CTL* ∩ LT L. An abstract path π^{♯} is a spurious counterexample if π_{0}^{♯} |̸= φ and γ(π^{♯}) = ∅.

The following theorem relates spurious counterexamples with backward and forward completeness with respect to post[R] and p̃re[R] respectively. The idea is that if a counterexample is spurious for an abstraction ρ, then there exists a concrete state x for which ρ fails to be forward complete for post[R] in x. The proof relies upon the fact that for spurious counterexamples π^{♯}, γ(π^{♯}) = ∅ and therefore there exists a concrete state x from which there is no forward transition into an abstract state, while there is a forward transition from ρ({x}). This clearly violates completeness for post[R].

Theorem 4. Let (℘(Σ), α, S^{♯}, γ) be a GI and ρ = γ∘α. Let φ ∈ ∀CTL* and π^{♯} be a counterexample. If π^{♯} is spurious then there exists i ∈ ℕ such that ∀x ∈ γ(π_{i}^{♯}) reachable from the states in I, i.e., γ(π_{0}^{♯}) ∩ I, it holds that:

ρ(post[R](ρ({x}))) ≠ ρ(post[R]({x})).

In particular, by Theorem 4, if π^{♯} is spurious then there exists π ∈ γ(π^{♯}) and x ∈ π such that ρ(post[R](ρ({x}))) ≠ ρ(post[R]({x})), or equivalently, by Proposition 4, there exists x ∈ π such that ρ(p̃re[R](ρ({x}))) ≠ p̃re[R](ρ({x})).

The complete shell abstract domain refinement can therefore be used to systematically refine abstract model-checking in order to eliminate spurious counterexamples. In particular, the machinery developed in [2] to eliminate spurious counterexamples in abstract Kripke structures can be formally reduced to the complete shell refinement operation introduced in [14]. The following example, taken from [2], shows this phenomenon.

Example 3. Consider a program with a variable whose values range in the following interval D = [1, 12] and which is represented by a transition system with states Σ = { 1, ⋯, 12 }, initial states I = { 1, 2, 3, 7, 8, 10, 11 } and transition relation:

R = \{ \begin{matrix}⟨1, 4⟩, ⟨2, 5⟩, ⟨3, 6⟩, ⟨4, 9⟩, ⟨5, 9⟩, ⟨6, 6⟩, ⟨7, 12⟩, \\ ⟨8, 8⟩, ⟨9, 9⟩, ⟨10, 10⟩, ⟨11, 11⟩, ⟨12, 12⟩ \end{matrix} \}

Let S^{♯} be the set of four abstract states S^{♯} = { ˆ1, ˆ2, ˆ3, ˆ4 }, corresponding to the equivalence classes of concrete states {1, 2, 3}, {4, 5, 6}, {7, 8, 9}, and {10, 11, 12}. Suppose that a model-checker gives an abstract counterexample π^{♯} = ˆ1, ˆ2, ˆ3, ˆ4. It is easy to see that π^{♯} is spurious, in fact, this abstract trace does not correspond to any concrete trace in the transition system. By Theorem 4 we can note that γ(ˆ3) = { 7, 8, 9 }, moreover only the concrete state 9 of this set is reachable from initial states in I, but it does not have any transition into a different concrete state. Therefore 9 does not have a transition to a state which is abstracted by ˆ4.

Note that, if there exists π ∈ γ(π^{♯}) and x ∈ π such that ρ(post[R]({x})) ≠ ρ(post[R](ρ({x}))) then this may not imply that π^{♯} is spurious. Consider for instance the abstract path π^{♯} = ˆ1, ˆ2, ˆ3 of Example 3. It is easy to check that ρ(post[R](ρ({ 6 }))) = [4, 9], whereas ρ(post[R]({ 6 })) = [4, 6], but π^{♯} corresponds to the concrete paths 1, 4, 9 and 1, 5, 9. Therefore, the complete shell refinement may induce a too strong refinement in the domain with respect to what is strictly necessary to remove spurious counterexamples, as shown in the following example. This phenomenon can be controlled by checking, at each iterate in the gfp-computation of the complete shell, the presence of spurious counterexamples.

Example 4. Consider the transition system in Example 3. Let (℘([1, 12]), α, A, γ) be the corresponding GI, with A = ℘({[1, 3], [4, 6], [7, 9], [10, 12]}). By Theorem 1 and Proposition 4, the ℬ-complete shell gfp(λX. γ∘α ⊓ ℛ_{post[R]}^{ℬ}(X)) is obtained as the limit of the sequence of abstract domains {A^{i}}_{i∈ℕ} defined as follows:

A^{i} = \{ \begin{matrix}A & if i = 0 \\ ℳ(p̃re[R](A^{i−1}) ∪ A) & otherwise \end{matrix}

This sequence of abstract domains converges in three steps to the fix-point. Each abstract domain A^{i} induces a refined partition according to Proposition 2 in the following way:

Domains  Refined partition
A^{0} ⟶  {[1, 3], [4, 6], [7, 9], [10, 12]}
A^{1} ⟶  {[1, 3], [4, 5], [6, 6], [7, 7], [8, 9], [10, 12]}
A^{2} ⟶ {[1, 2], [3, 3], [4, 5], [6, 6], [7, 7], [8, 9], [10, 12]} (fix-point)

Consider the partition induced by A^{1}. The new abstract states {4, 5} and {7} are introduced by computing the maximal inverse image of post[R] in the states {10, 11, 12} and {7, 8, 9}, whereas the states {6} and {8, 9} are added to obtain a partition of ℘([1, 12]). Now consider the partition induced by A^{2}. The new abstract states {3} and {1, 2} are introduced by computing respectively the inverse image of post[R] in the states {6} and {4, 5} of A^{1}. It is worth noting that the partition induced by A^{1} is sufficient to remove any spurious counterexample. Therefore the refinement process can be stopped after the first iteration. This condition can be verified by checking counterexamples at each iterates in the fix-point computation.

7 Complete data-flow analysis: A different perspective

In this section we sketch, by means of a simple example, how we can design sound and complete data-flow analysis algorithms as complete model-checking of abstract interpretations. Once again, completeness is achieved by removing spurious counterexamples.

The idea of data-flow analysis as model-checking goes back to Steffen’s pioneering work [22]. More recently Schmidt [20, 21] showed that data-flow analysis problems can be formulated as model-checking problems of a trace-based abstract interpretation of operational semantics. Intuitively, the concrete semantics of a program is a tree whose paths represent execution traces and whose nodes display the program’s changing states. The abstract interpretation of the semantics of a program is also a computation tree, but whose nodes contain the abstraction of information contained in concrete states. To be useful, a program abstract computation tree must safely simulate the concrete computation tree that it represents. Thus any property that holds in an abstract tree must also hold for all the corresponding concrete trees. However, the dual notion of completeness does not hold in general, namely the properties that do not hold in the abstract may not be counterexamples for the concrete.

                                        Concrete semantics transitions
                                        Val=Int

0 ⊢ x = 0 → 0 ⊢ x := succ(x) 0 ⊢ x := succ(x) → 1 ⊢ x = 0 + (n + 1) ⊢ x = 0 → +(n + 1) ⊢ x > 0 + (n + 1) ⊢ x > 0 → +(n + 1) ⊢ x := −x + (n + 1) ⊢ x := −x → −(n + 1) ⊢ x > 0 − (n + 1) ⊢ x = 0 → −(n + 1) ⊢ x > 0 − (n + 1) ⊢ x > 0 → −(n + 1) ⊢ x := 0 − (n + 1) ⊢ x := 0 → 0 ⊢ x = 0

Fig. 3. Flowchart and concrete interpretation

Let us consider the flowchart program depicted in Fig. 3. Its concrete semantics is expressed as a set of transition rules between program states. A program state is an element of V al × ProgramPoint and is written as n ⊢ p, where n is the value of the variable x at program point p. Note that in this example the concrete computation tree is an infinite execution trace. The fundamental idea in Schmidt’s trace-based abstract interpretation [20, 21] is to replace an execution trace of the program by transition rules that use abstract values instead of run-time values. The result is an abstract computation tree, where multiple possible executions traces are presented by a non-deterministic branching in the abstract tree.

In the example above we consider a program analysis which detects whether x is zero or not. This corresponds to replace the concrete domain V al = Int by AbsV al = {0, ≠ 0} and by rewriting the state transition rules accordingly. More in detail, we consider a function β : V al → AbsV al, which maps concrete values to their most precise abstractions. For the example, in Fig. 3, we have β(0) = 0 and β(±(n + 1)) = ≠ 0. Moreover, the following homomorphism property is necessary in order to let the abstract transitions correctly simulate the concrete ones: if (v ⊢ p) → (v′ ⊢ p′) is a concrete transition, then there must exist an abstract transition, (β(v) ⊢ p) → (a′ ⊢ p′), such that β(v′) ≤ a′, where ≤ is the approximation order between abstract values. The resulting abstract semantics transitions are shown in Fig. 4:

 Abstract semantics transitions

0 ⊢ x = 0 → 0 ⊢ x := succ(x) 0 ⊢ x := succ(x) →≠ 0 ⊢ x = 0 ≠ 0 ⊢ x = 0 →≠ 0 ⊢ x > 0 ≠ 0 ⊢ x > 0 →≠ 0 ⊢ x := −x ≠ 0 ⊢ x > 0 →≠ 0 ⊢ x := 0 ≠ 0 ⊢ x := −x →≠ 0 ⊢ x > 0 ≠ 0 ⊢ x := 0 → 0 ⊢ x = 0

                                  Refined Abstract semantics transitions

0 ⊢ x = 0 → 0 ⊢ x := succ(x) 0 ⊢ x := succ(x) → + ⊢ x = 0 + ⊢ x = 0 → + ⊢ x > 0 + ⊢ x > 0 → + ⊢ x := −x + ⊢ x := −x → − ⊢ x > 0 − ⊢ x = 0 → − ⊢ x > 0 − ⊢ x > 0 → − ⊢ x := 0 − ⊢ x := 0 → 0 ⊢ x := 0

Fig. 4. Abstract Interpretation of flowchart

Consider the safety CTL formula φ = ∀G∀F (x = 0) specifying that for each program state in any trace it is possible to reach a program state where the value of the variable x is 0. It is easy to check that the abstract tree does not satisfy this property because there exists an infinite trace ≠ 0 ⊢ x = 0 →≠ 0 ⊢ x > 0 →≠ 0 ⊢ x := −x →≠ 0 ⊢ x > 0 → … that invalidates the specification. In this case, the abstraction is too rough because this is an infinite abstract trace that does not correspond to any concrete trace, i.e., we have found a spurious counterexample for φ.

In order to find a sound and complete trace based abstract interpretation, we have to refine the abstraction. By applying the backward complete shell refinement for post[R], with R being the transition relation specified above, we obtain a refined model which includes the abstract values {0, +, −, ≠ 0}. In this case, the abstraction function is such that β(0) = 0, β(+(n + 1)) = + and β(−(n+1)) = −. The resulting refined abstract semantics transitions, according to Definition 4, are shown in Fig. 4. It is easy to check that the refined abstract tree now satisfies the property φ.

8 Conclusions

In this work we have studied the impact of the notions of forward and backward completeness in abstract interpretation based model-checking. Our results allows us to apply standard abstract interpretation theory to refine abstract models when they result too rough for verifying temporal properties of interest. We have proved that the precision of the abstract model-checking problem for a Kripke structure 𝕄 = ⟨Σ, I, R, ∥ ∘ ∥⟩ is strictly connected to the precision of the underlying abstract domain, and that spurious counterexamples can be removed by considering the complete shell of the abstract domain with respect to the post[R] predicate transformer.

It is particularly interesting to study what kind of counterexamples that can be removed when the refinement is computed with respect to an arbitrary function f, possibly different from post[R]. In this case our results allows us to formally derive the structure of those counterexamples that can be removed by an arbitrary domain refinement operation, provided that this operation can be encoded as a complete shell, namely it corresponds to the complete shell refinement 𝒮_{f}^{ℬ} with respect to a given function f. It is easy to see that if 𝕄^{A} is an abstract Kripke structure associated with an abstract domain A and a concrete transition system ⟨Σ, R⟩, the refinement operation 𝒮_{f}^{ℬ} returns a refined Kripke structure 𝕄^{𝒮_{f}^{ℬ} (A)} according to Proposition 2 which, for a given formula φ, removes all the counterexamples that corresponds to the traces in a modified (simplified) transition system ⟨Σ, R ∧ R_{f}⟩. This new transition system includes only those transitions that satisfy both the original relation R and the relation associated with f. The consequences of this observation in static program analysis by abstract model checking are under investigation.

Acknowledgments

The interest in applying the constructive characterization of completeness in [14] to Clarke’s spurious counterexamples came to our attention in a discussion we had with Andreas Podelsky during a breakfast at Place de la Sorbonne, Paris, in July 2000. We wish to thank Andreas for having pointed to us the work of Clarke, Francesco Ranzato, and the anonymous referees for their helpful comments. Part of this work was carried out while the authors were visiting the Laboratoire d’Informatique, Ècole Polytechnique, Palaiseau, France. This work has been supported by the Italian MURST project: “Certificazione automatica di programmi mediante interpretazione astratta”.

References

1. E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent system using temporal logic specification. ACM Trans. Program. Lang. Syst., 8(2):244–263, 1986.

2. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. of the 12th Internat. Conf. on Computer Aided Verification (CAV ’00 ), volume 1855 of Lecture Notes in Computer Science, pages 154–169. Springer-Verlag, Berlin, 2000.

3. E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Trans. Program. Lang. Syst., 16(5):1512–1542, 1994.

4. P. Cousot. Types as abstract interpretations (Invited Paper). In Conference Record of the 24th ACM Symp. on Principles of Programming Languages (POPL ’97 ), pages 316–331. ACM Press, New York, 1997.

5. P. Cousot. Partial completeness of abstract fixpoint checking, invited paper. In Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA’2000, Lecture Notes in Artificial Intelligence 1864, pages 1–25, Horseshoe Bay, Texas, USA, 26–29 July 2000. Springer-Verlag, Berlin, Germany.

6. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symp. on Principles of Programming Languages (POPL ’77 ), pages 238–252. ACM Press, New York, 1977.

7. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL ’79 ), pages 269–282. ACM Press, New York, 1979.

8. P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69–95, 1999.

9. P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12–25, Boston, Mass., January 2000. ACM Press, New York, NY.

10. D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst., 19(2):253–291, 1997.

11. E. A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, Amsterdam and The MIT Press, Cambridge, Mass., 1990.

12. G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.

13. R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. of the 24th Internat. Colloq. on Automata, Languages and Programming (ICALP ’97 ), volume 1256 of Lecture Notes in Computer Science, pages 771–781. Springer-Verlag, Berlin, 1997.

14. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretation complete. Journal of the ACM, 47(2):361–416, March 2000.

15. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:1–36, 1995.

16. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, Berlin, 1992.

17. M. Müller-Olm, D. Schmidt, and B. Steffen. Model-checking. A tutorial introduction. In G. Filé, editor, Proceedings of the International Static Analysis Symposium (SAS ’99 ), volume 1694 of Lecture Notes in Computer Science, pages 330–354. Springer-Verlag, Berlin, 1999.

18. A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. of the ACM Symp. on Partial Evaluation and Program Manipulation (PEPM ’93 ), pages 179–185. ACM Press, New York, 1993.

19. F. Ranzato. On the completeness of model checking. In Proc. of European Symposium on Programming (ESOP ’01 ), Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001.

20. D. A. Schmidt. Data flow analysis is model checking of abstract interpretation. In Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’98 ), pages 38–48. ACM Press, New York, 1998.

21. D. A. Schmidt. Trace-based abstract interpretation of operational semantics. Lisp and Symbolic Computation, 10(3):237–271, 1998.

22. B. Steffen. Data flow analysis as model checking. In A. Meyer, editor, Proc. of Theoretical aspects of computer software (TACS ’91 ), volume 526 of Lecture Notes in Computer Science, pages 346–364. Springer-Verlag, Berlin, 1991.