Abstract Interpretation Using Typed Decision Graphs

Laurent Mauborgne^{⋆}

LIENS, École Normale Supérieure, 45 rue d’Ulm, 75230 Paris cedex 05, France

Abstract. This article presents a way of implementing abstract interpretations that can be very efficient. The improvement lies in the use of a symbolic representation of boolean functions called Typed Decision Graphs (TDGs), a refinement of Binary Decision Diagrams. A general procedure for using this representation in abstract interpretation is given; we examine in particular the possibility of encoding higher order functions into TDGs. Moreover, this representation is used to design a widening operator based on the size of the objects represented, so that abstract interpretations will not fail due to insufficient memory. This approach is illustrated on strictness analysis of higher-order functions, showing a great increase in efficiency.

1 Introduction

One of the basic problems of program analysis is that, even theoretically speaking, there are properties of programs which cannot always be computed, such as termination. A way to circumvent this difficulty is to allow for partial or approximate answers. Abstract interpretation is the theoretical framework to design automatic program analysis based on sound approximations. Although this theory deals very well with many problems of program analysis, it may become unusable in practice when the analysis is too precise, because of the amount of memory, or time required. The goal of this article is to show that it is sometimes possible, using compact representations of boolean functions, not only to increase significantly the efficiency of the analysis, but also to balance the trade off between precision and efficiency during the analysis.

In the second section of this paper, we will describe the symbolic representation of boolean functions. In section 3, we will show how to use it in abstract interpretation. We will expose in detail the coding of higher order functions through TDGs, and the use of those graphs in conjunction with data approximation. The last section is dedicated to a complete example of abstract interpretation using TDGs: strictness analysis.

Because the most general framework of abstract interpretation is mathematical, most elements of this paper have been described mathematically. Consequently some of the principles may come through unclear. The reader who is not familiar with some concepts or does not want to read mathematical formulas

⋆ email: Laurent.Mauborgne@ens.fr

should read the informal descriptions, which will give an idea of what is going on. On the other hand, if the reader is already familiar with one notions, he is invited to skip the informal presentation corresponding to this notion.

2 Typed Decision Graphs

Typed Decision Graphs [9], or TDGs, are powerful symbolic representations of boolean functions. They are a refinement of the well-known Binary Decision Diagrams [6], or BDD, which are already widely used in many fields, such as circuits synthesis and verification [11, 12, 15], or protocols verification [13, 14] but mostly unused in abstract interpretation (but see [20, 21]). The purpose of this paper is to show that this representation of boolean functions can in some cases have major applications in abstract interpretation.

2.1 Informal Presentation of Binary Decision Diagrams

A BDD, as introduced by Bryant in [6], is a compact representation of the Shannon tree of a boolean expression.

Shannon Trees Shannon trees are used to represent boolean expressions. They describe a way to evaluate the expression. First evaluate the value of one of the boolean variables of the expression. If this variable is true, then we can represent a boolean expression containing less variables, and if it is false, we represent another boolean expression containing less variables. If, in the end, the boolean expression does not contain any more variable, then its value is either true or

false.

As a result, each node of a Shannon tree is associated to a variable, the left subtree represents the boolean expression when this variable is false and the right subtree when it’s true.

In order to have a unique representation of a given boolean expression, the variables of the expression are to be taken in a predetermined order.

For example, let’s consider the following expression: (x∧y)∨(y∧¬z)∨(z∧¬y). We can represent this expression f using a table:

\begin{matrix}x & 0 & 0 & 0 & 0 & 1 & 1 & 1 & 1 \\ y & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 \\ z & 0 & 1 & 0 & 1 & 0 & 1 & 0 & 1 \\ f & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 1 \end{matrix}

If x < y < z, the Shannon tree representing f will be:

[figure: x; y; y; z; z; z; z; 0; 1; 1; 0; 0; 1; 1; 1]

Reduction Rules Once a boolean expression is represented by a Shannon tree, it is easy to see how to gain space. First, there’s no need to duplicate subtrees. The action of merging redundant subtrees is called sharing. Instead of having a binary tree, we will have a directed acyclic graph. In order to recognize left subtrees from right subtrees we will draw the formers with dashed line. In our example, f will be represented by:

[figure: x; y; y; z; z; z; 0; 1]

The second reduction rule is the elimination of useless nodes, namely nodes where the different possible values of the variable lead to the same result. After this step, we have the BDD representing f:

[figure: x; y; y; z; z; 0; 1]

2.2 Formalization Work on Binary Decision Diagrams

Abstract interpretation is a theoretical and formalized approach of program analysis. So, to use BDDs in abstract interpretation we need to formalize them very precisely. We shall first define the objects encoded by BDDs, which are boolean functions and the names of the variables used to calculate them.

Let Var be a totally ordered set of variables. The order on Var will be noted <^{v}.

Var_{n} =^{def} {V ⊆ Var | |V | = n}, where |V | is the size of the set V.

To simplify our notations, we always order the indexes of set of variables according to the order on Var. So when we write {x_{1}, …, x_{n}} ∈ Var_{n} it means ∀i, 1 ≤ i ≤ n, x_{i} ∈ Var and x_{1} <^{v} … <^{v} x_{n}.

B_{n} =^{def} Var_{n} × ({0, 1}^{n} → {0, 1})
B =^{def} ⋃_{n} B_{n}

The pair ({x_{1}, …, x_{n}}, f) ∈ B_{n}, also noted f(x_{1}, …, x_{n}) in this paper, is the semantics of a boolean expression with n (free) variables x_{1} <^{v} … <^{v} x_{n} whose value is given by the function f. The variable x alone stands for ({x}, Id). The symbols ¬, ∧ and ∨ have the usual meaning of the boolean operators “not”, “and” and “or”. We define V(f(x_{1}, …, x_{n})) =^{def} {x_{1}, …, x_{n}}.

BDDs are based on Shannon trees, whose uniqueness is insured by Shannon’s expansion theorem [1]. Written in our formalism, this theorem is:

Theorem 1 (Shannon’s expansion). Let f(x_{1}, …, x_{n}) ∈ B_{n}. ∀i, 1 ≤ i ≤ n, ∃!(f\overline{x_{i}}, f_{x_{i}}) ∈ (B_{n−1} × B_{n−1}) such that:

f(x_{1}, …, x_{n}) = (¬x_{i} ∧ f\overline{x_{i}}) ∨ (x_{i} ∧ f_{x_{i}})

A Shannon tree is a binary tree labeled with variables, 0 or 1. A binary tree T can be defined as a partial function from {0, 1}^{⋆}, the set of all finite words on {0, 1}, to the set of labels, with the prefix closure property i.e. the domain is not empty, and if a word uv is in its domain, then u is in its domain too^{1}. The Shannon tree representing f(x_{1}, …, x_{n}) is defined as follows:

St(f(x_{1}, …, x_{n}))(u) =^{def} if |u| < n then x_{|u|+1}
if u = a_{1}a_{2} … a_{n} then f(a_{1}, a_{2}, …, a_{n})

where |u| is the length of u.

As explained in the informal presentation, BDDs are compact representations of Shannon trees, obtained by enforcing the two simple reduction rules: sharing and elimination.

Sharing. This operation transforms the tree into a directed acyclic graph (DAG) by sharing isomorphic subtrees. A binary decision DAG (BDD) can be defined recursively as being either a node N of Var×bdd×bdd or a leaf in {0, 1}.

1 uv is the concatenation of u and v

As the transformation is described by the share function, it is obviously still unique.

share(St) =^{def} if St = root(k) then k else N(St(ϵ), St\0, St\1)

where ϵ is the empty word, root(k) is the tree with domain {ϵ} and value k, and T \u is the subtree of T with domain dom(T \u) =^{def} {v|uv ∈ dom(T)} and such

that T \u(v) =^{def} T (uv).

The sharing results from the fact that if two subtrees are isomorphic the mathematical objects representing these subtrees are equal. The results of share on them are obviously identical.

Elimination of Superfluous Nodes. Once again, the transformation can be written as transformation rules; the representation is still unique.

supp(N(x, d_{1}, d_{2})) = if d_{1} = d_{2} then supp(d_{1}) else N(x, supp(d_{1}), supp(d_{2}))

After applying this rule, a BDD does no longer represent one function of B, but all the functions whose results are the same regardless of the assignment of additional variables absent in the BDD. For example, if ∀x, y, z, f(x, y, z) = g(y) then f(x, y, z) and g(y) are represented by the same BDD. This drawback does not really matter for this work, because what we really manipulate are functions from {0, 1}^{ω} to {0, 1}.

2.3 TDGs

To reduce the size of the graph even further, we go back to Shannon trees and try to produce new isomorphic subtrees. Then we will apply the same reduction rules.

Typed Shannon Trees. The idea of typed Shannon trees [3] came from the remark that:

¬f = ¬x ∧ ¬f\overline{x} ∨ x ∧ ¬f_{x}

This means that as far as Shannon trees are concerned, f and ¬f are identical except for the leaves: 0 becoming 1 and 1 becoming 0. So instead of having two different trees, we only need one tree and a sign. Typed Shannon trees are merely trees with signs. To be more precise, the labeling set becomes {−, +} × (Var ⋃{0, 1}). And if T such that T (ϵ) = (s, l) represents f then ¬f can be represented by T if you change T (ϵ) in (−s, l).

Now, the problem is that when using simple Shannon trees and just adding signs, canonicity is lost: 0 can be represented by (+, 0) or (−, 1) for example. Let us simply make a choice, once for all. Here is one that provides good results for the size of the graph [10]:

Tst(f(x_{1}, …, x_{n}))(a_{1} … a_{i}) =^{def} if f(a_{1}, …, a_{i}, 1, …, 1) = 1
then (+, St(f(x_{1}, …, x_{n}))(a_{1} … a_{i}))
else (−, St(¬f(x_{1}, …, x_{n}))(a_{1} … a_{i}))

The resulting tree is represented in fig. 1. The signs have been put on the edges instead of the labels, and only minus have been represented to get a more compact representation.

[figure: x; −; y; −; y; z; −; z; −; z; −; z; 1; 1; 1; 1; 1; 1; 1; 1]

Fig. 1. Typed Shannon tree.

Resulting Graph. Now, if we simply apply the same reduction rules as for a BDD, still assuring the uniqueness of the representation, and we get Typed Decision Graphs. To know the value of the function for a given assignment, follow the same method as for BDD, counting the number of − in the path. If this number is odd then the result is 0, if it is even, 1.

[figure: x; −; y; −; y; z; −; 1; x; y; −; z; −; 1]

Fig. 2. The TDG for f(x, y, z) = (x ∧ y) ∨ (y ∧ ¬z) ∨ (z ∧ ¬y), and f(y, x, z) = (y ∧ x) ∨ (x ∧ ¬z) ∨ (z ∧ ¬x).

The size of the TDGs looks quite reasonable, and it is in most case. But there are still cases where it is exponential in the number of its variables [16]. If we restrict the representation to boolean functions without explicit variables^{2},

2 It is possible to represent boolean functions with explicit variables using boolean functions without explicit variables, so it could still be useful.

then it is sometimes possible to reduce the size of the TDG representing the function by changing the order of the variables^{3}. But there are cases where the representation is still exponential, whatever the order of the variables.

2.4 Operators on TDGs

Not only does this representation save space, but it saves time too, assuming the operators on boolean functions are correctly translated.

An operator is a function from B^{n} to B. The key property that allows for a fast computation of operators is orthogonality [16].

Definition 1. Let Op be a n-operator. Op is said orthogonal iff:

\{ \begin{matrix}∀f_{1}, …, f_{n} ∈ B, ∀x ∈ Var, \\ Op(f_{1}, …, f_{n}) = ¬x ∧ Op(f_{1}\overline{x}, …, f_{n}\overline{x}) ∨ x ∧ Op(f_{1}_{x}, …, f_{n}_{x}) \\ ∀k_{1}, …, k_{n} ∈ B_{0}, Op(k_{1}, …, k_{n}) ∈ B_{0} \end{matrix}

For example, ¬, ∧ and ∨ are orthogonal operators.

An orthogonal operator on TDGs can be calculated by the following algorithm:

Op^{TDG}(k_{1}, …, k_{n}) = Op(k_{1}, …, k_{n})

Op^{TDG}(f_{1}, …, f_{n}) =

let x = inf ⋃_{1≤i≤n} V(f_{i}),

let T_{1} = Op^{TDG}(f_{1}\overline{x}, …, f_{n}\overline{x}) and T_{2} = Op^{TDG}(f_{1}_{x}, …, f_{n}_{x}) if T_{1} = T_{2} then T_{1}

       if the sign of T_{2} is + then (+, N(x, T_{1}, T_{2}))

if the sign of T_{2} is − then (−, N(x, ¬T_{1}, ¬T_{2}))

The proof of this algorithm is by induction on | ⋃_{1≤i≤n} V(f_{i})|.

If we keep in memory the intermediate results, then the total cost in time of the operator is O(|f_{1}|×…×|f_{n}|), where |f_{i}| is the number of nodes of the TDG representing f_{i}. So most of the time^{4}, calculation with orthogonal operators over TDG are quite fast.

3 Abstract Interpretation

3.1 Informal Presentation of Abstract Interpretation

Abstract interpretation is a very general and formalized framework allowing to deal with approximations. The rule of signs (positive multiplied by positive is

3 See fig. 2 for an example. 4 see section 2.3.

positive, etc.) can be seen as an abstract interpretation: the concrete domain (real numbers) is abstracted by approximate values in an abstract domain ({positive numbers, negative numbers, zero}), and the concrete operation (multiplication) is approximated by an abstract operation (the rule of signs).

The aspects of abstract interpretation that we will use are:

– The possibility to lift automatically an abstract interpretation. That is to say, given domains and their approximations, the possibility to approximate functions over those domains.

– Widening operators. When the semantics of a program can be expressed as the limit of the iteration of a given function (often given by the syntax of the program), the abstract semantic can also be expressed as the limit of the iteration of an abstract function. But in some cases, more approximation is needed. Then abstract interpretation provides the possibility of using a widening, which is an operator that alters the iteration, generally speeding it, but at the cost of wider approximation.

3.2 Recall of Important Aspects

Taking the most general framework [17], all the possible behaviors of programs are described in a standard semantics. From the point of view of abstract interpretation however, only a certain class of these behaviors is interesting. This class is the collecting semantics. Then the abstract semantics is usually an approximation of the collecting semantics^{5} that keeps for example only invariance properties. All those properties are taken from sets called semantic domains, and one of the most important tasks of an abstract interpretation is to describe the relations between the abstract semantic domain P^{♯} and the concrete semantic domain P^{♮}.

The concrete semantics of a program is often given by the limit of the iteration of a concrete semantic function, F^{♮}, starting from a basis ⊥^{♮}, and using an inductive join ⨿^{♮} to go to limit ordinals.

F^{♮0} =^{def} ⊥^{♮}
F^{♮λ+1} =^{def} F^{♮}(F^{♮λ})
F^{♮λ} =^{def} ⨿_{β<λ}^{♮}F^{♮β} when λ > 0 is a limit ordinal

To ensure convergence, P^{♮} is often associated to a complete lattice structure, the limit of the iteration being then the least fixpoint of F^{♮} (lfp(F^{♮})). The same ideas apply to determine the abstract semantics of a program.

The relation between the concrete and abstract semantic can be described by a soundness relation σ. ⟨c, a⟩ ∈ σ meaning that a is a sound approximation of the property c. Moreover, one will want the approximation both sound and

5 the abstract semantics can be an approximation of whatever semantics, even another abstract semantics, so for the purpose of relations between semantics, the approximated one will always be called concrete semantics.

“good”. To define this notion, abstract interpretation uses an approximation order on properties, ⪯. The soundness relation σ is then supposed to respect the approximation order, namely if a ⪯^{♯} a′ and ⟨c, a⟩ ∈ σ then ⟨c, a′⟩ ∈ σ. In this case, we say that a is a better approximation than a′. In the most ideal case, there will exist one best approximation for each property of P^{♮}. It will be given by an abstract function α.

Sometimes, there is none or many best approximation. Even when there is only one, the computation of the abstract property (possibly obtained by an abstract iteration^{6}) may be too long or even infinite. A solution for all these problems is the use of a widening operator. A widening operator is a partial function ▽^{♯} from ℘(P^{♯}) to P^{♯} such that:

(▽^{♯}A exists) ⇒ (∀c ∈ P^{♮}: (∃a ∈ A: ⟨c, a⟩ ∈ σ) ⇒ (⟨c, ▽^{♯}A⟩ ∈ σ))

Then we can use the following abstract iteration with widening:

F^{♯↑0} =^{def} ⊥^{♯}
F^{♯↑λ+1} =^{def} ▽^{♯}{F^{♯↑λ}, F^{♯}(F^{♯↑λ})}
F^{♯↑λ} =^{def} ▽^{♯}(⋃{F^{♯↑β}|β < λ}) when λ > 0 is a limit ordinal

If moreover there is an abstract function α, and ▽^{♯} satisfy:

▽^{♯}A exists ∧ c ∈ P^{♮} ∧ a ∈ A ∧ α(c) ⪯^{♯} a ⇒ α(c) ⪯^{♯} ▽^{♯}A
⨿_{i∈I}^{♯}c_{i} exists ∧ ▽_{i∈I}^{♯}a_{i} exists ∧ ∀i ∈ I: α(c_{i}) ⪯^{♯} a_{i} ⇒ α (⨿_{i∈I}^{♯}c_{i}) ⪯^{♯} ▽_{i∈I}^{♯}a_{i}.

Consequently if the concrete iteration sequence and abstract iteration with widening are convergent then their limits F^{♮ϵ} and F^{♯↑ε} are such that α(F^{♮ϵ}) ⪯^{♯} F^{♯↑ε}.

In fact, that limit might be a post-fixpoint, in which case the result can be refined using a narrowing operator [4]. For more results and details on abstract interpretation, see [17].

3.3 Using TDGs

Basically, TDGs can be used to encode the data handled by the abstract interpretation. Let’s call β the encoding between P^{♯} and B, F^{♭} the operator induced by the abstract operator. Considering the properties of TDGs described in section 2 —i.e. their compactness and the efficiency of their operators— the replacement of the abstract iteration by the iteration of F^{♭} on B will in general fill considerably less space, and hopefully take less time than the iteration on classical representations. But, while it is theoretically always possible to find an encoding, not all encodings have these properties. As a trivial example, a coding that associates a variable (and whatever function from {0, 1} to {0, 1}) to each element of P^{♯} will just fill more space.

6 that is to say the limit of the F^{♯λ}.

Although we have no general rule to find a good encoding, we provide some generic tools that can help the design or the use of such an encoding. The first tool will transform encodings of first order functions into encodings of higher order functions. This tool makes the design of the encoding easier, because the encoding of first order functions only is needed. Moreover, it applies to the encoding of the abstract function itself into TDGs. The second tool is a widening operator taking advantage of the structure of the TDGs. It can be used in any abstract interpretation to produce approximations based on the complexity only.

Lifting an Abstract Interpretation.

Informal Presentation. Given the abstractions over two domains, it is possible to abstract the set of functions over those two domains by using the set of functions over the associated abstract domains. If those two domains are already encoded into BDDs, it is then possible to code the functions over those domains using BDDs. This cannot be straightforward, as functions over BDDs are not boolean functions. The point in transforming these functions into BDDs is to replace the variables representing BDDs by (more) boolean variables.

Bounding the number of possible BDDs the variable can represent is a necessary condition to achieve that transformation. So we choose to bound the number of variables of the BDDs that the variable represents. For example, we will work under a limit of one boolean variable for the BDD variable f. For a better understanding, let us come back to Shannon trees —the same can be done with BDDs—. We can represent the function that takes f and gives a boolean expression almost like a Shannon tree. The difference is that, there being four different boolean expression with at most one boolean variable, one should have four subtrees coming from f. The tree will have the following structure:

[figure: f; 0; y; ¬y; 1; _{tree_{1}}; _{tree_{2}}; _{tree_{3}}; _{tree_{4}}]

This variable over BDDs can be replaced by two boolean variables, x_{1} and x_{2}, chosen to be taken before any variable in the subtrees:

[figure: x_{1}; x_{2}∧y; ¬y∨x_{2}∧y; x_{2}; 0; y; x_{2}; ¬y; 1; _{tree_{1}}; _{tree_{2}}; _{tree_{3}}; _{tree_{4}}]

So we have replaced f by the following variable boolean expression with at most one boolean variable y: ¬y ∧x_{1} ∨y ∧x_{2}. This construction will be extended and justified in the next paragraph.

Technical Aspect. Let P_{1}^{♯} and P_{2}^{♯} be two abstract semantics encoded into TDGs by β_{1} and β_{2}. Moreover we will suppose that P_{1}^{♮}(⪯_{1}^{♮}) \overleftarrow{⟶}^{γ_{1}}_{α_{1}} P_{1}^{♯}(⪯_{1}^{♯}) and P_{2}^{♮}(⪯_{2}^{♮} ) \overleftarrow{⟶}^{γ_{2}}_{α_{2}} P_{2}^{♯}(⪯_{2}^{♯}) are Galois connections^{7}. As suggested in [2], such Galois connections can be lifted to functions:

P_{1}^{♮} ⟼^{m} P_{2}^{♮}(⪯^{♮}) \overleftarrow{⟶}^{λg.γ_{2}∘g∘α_{1}}_{λf.α_{2}∘f∘γ_{1}} P_{1}^{♯} ⟼^{m} P_{2}^{♯}(⪯^{♯})

is also a Galois connection, assuming ⪯ is the pointwise ordering^{8}, and A ⟼^{m} B is the set of monotonic functions from A to B.

The lifted semantic domain contains functions from P_{1}^{♯} to P_{2}^{♯}. It means that if we want to extend directly the encoding to the lifted domain, we will need functions over boolean functions, which are not directly representable by TDGs. This is because we cannot make a binary choice after testing a functional variable, as such a variable can take more than two different values. A solution is to transform the tests of functional variables into a sequence of binary tests in required number.

But a variable representing a TDG could take an infinite number of value, as B is infinite. Accordingly, we will first restrain the set encoded into TDGs to B^{↑} =^{def} ⋃_{n} B_{n}^{↑}, where B_{n}^{↑} =^{def} ({0, 1}^{n} → {0, 1}) → B, Var_{n}^{↑} being the set of variables used in B_{n}^{↑} and Var^{↑} =^{def} ⋃_{n} Var_{n}^{↑}.

Let λf.G ∈ B^{↑}; then ∃n, f ∈ Var_{n}^{↑}, so that testing a value of f can be replaced by testing the value of a finite set of binary variables. Three steps will occur when transforming this expression into a boolean expression: first create this set of binary variables (using v(f)), second link an assignment to this set of variable to an assignment to f (using build(v(f))), at last replace f in λf.G by the variable function just built. To understand those stages better, we will go through them on a simple example, λf.λx.fx^{9}. In this example, f ∈ Var_{1}^{↑}.

For the construction of the set of boolean variables, we use Shannon’s expansion theorem in the following form: a variable f of Var_{n+1}^{↑} is equivalent to a pair of variables (else_{n}(f), then_{n}(f)) ∈ Var_{n}^{↑} × Var_{n}^{↑}, where else_{n}(f) represents the value of f when its first variable is false, and then_{n}(f) when it is true. As we want to ensure that those variables are distinct, we require the following properties for then_{n} and else_{n}: ∀f, g ∈ Var_{n+1}^{↑}, then_{n}(f) ≠ else_{n}(g) and both then_{n} and else_{n} are injections. We can now define the set of variables associated with a variable f of Var^{↑}, v(f) ∈ ℘(Var):

v(f) =^{def} {b(f)} if f ∈ Var_{0}^{↑}
v(f) =^{def} v(else_{n}(f)) ∪ v(then_{n}(f)) if f ∈ Var_{n+1}^{↑}

7 i.e. ∀c ∈ P^{♮}, ∀a ∈ P^{♯} : (c ⪯^{♮} γ(a)) ⟺ (α(c) ⪯^{♯} a). 8 f ⪯ g ⟺ ∀x ∈ P_{1}, f(x) ⪯_{2} g(x). 9 To distinguish between functional variables and elements of Var, elements of Var are

noted x, y, x_{i}, …, and functional variables f, g, …

where b is a bijection from Var_{0}^{↑} to Var. It is easy to prove by induction that v(f) is just a set of 2^{n} distinct boolean variables, {x_{1}, …, x_{2^{n}}}. Let us go back to the simple example, v(f) = {x_{1}, x_{2}}, with x_{2} ≠ x_{1}. Actually, two boolean variables are exactly what is needed to represent the four different possible values of f.

Now we build the variable function associated to this set of boolean variables, so that we can apply this set to boolean values.

build{x} =^{def} x
build{x_{1}, …, x_{2^{n}}} =^{def} λy.¬y ∧ build{x_{1}, …, x_{2^{n−1}}} ∨ y ∧ build{x_{2^{n−1}+1}, …, x_{2^{n}}}

Once again, this definition is justified by Shannon’s expansion theorem. In our example, build{x_{1}, x_{2}} = λy.¬y ∧ x_{1} ∨ y ∧ x_{2}.

It is now easy to translate the assignment of a variable f of Var_{n}^{↑} by F ∈ ({0, 1}^{n} → {0, 1}) into an assignment of v(f): just assign to each variable of v(f) the value of F applied to the correct boolean values, such that F equals build(v(f)) in which all variables of v(f) have been instantiated. So, for example, substituting the variable f of Var_{1}^{↑} by the function λx.¬x is the same as substituting v(f) = (x_{1}, x_{2}) by (1, 0).

We can now code B^{↑}. Let λf.G ∈ B^{↑}, then ∃n, f ∈ Var_{n}^{↑}. Let {y_{1}, …, y_{2^{n}}} = s(v(f)) where s is a permutation on Var such that y_{2^{n}} is less (for the order on Var) than the smallest possible variable appearing in G. Then if the encoding is called β^{↑}:

β^{↑}(λf.G) =^{def} λy_{1}, …, y_{2^{n}}.G[f/build{y_{1}, …, y_{2^{n}}}]

Example: β^{↑}(λf.λx.fx) = λx_{1}.λx_{2}.λx.¬x ∧ x_{1} ∨ x ∧ x_{2}.

We now have an encoding of P_{1→2}^{♯}, if we can code it into B^{↑}. To achieve this, we will assume the following hypothesis on β_{1}: for all variable of P_{1}^{♯} there exists a N such as each instantiation of the variable is coded in B_{n} with n ≤ N. Then β_{1}^{v} of such a variable is a variable in Var_{N}^{↑}. So

β_{1→2}(λf.G) =^{def} β^{↑}(λβ_{1}^{v}(f).β_{2}(G[f/β_{1}^{v}(f)]))

This coding is interesting for abstract functions too, because if G = lfp(F_{2}) then λf.G = lfp(F_{1→2}) where F_{1→2}(λx.y) =^{def} λx.F_{2}(y). So if F_{2}^{♯} is coded into TDG, F_{1→2}^{♯} can be coded into TDG too.

In the particular case where P_{2}^{♯} = P_{1}^{♯}, we have coded functions over P_{1}^{♯}. As abstract functions are just functions over P_{1}^{♯}, we can thus code them into TDG, making the iteration faster^{10}. To encode higher order functions on P_{1}^{♯}, we just have to iterate this construction, as now first order functions are just TDGs. For example, the second order function λg(λfλx.g(f(x))) can be encoded the following way: g ∈ V ar_{1}^{↑}, so v(g) = {z_{1}, z_{2}} and so β^{↑}(λg(λfλx.g(f(x)))) = λ(z_{1}, z_{2}, x_{1}, x_{2}, x).¬(¬x ∧ x_{1} ∨ x ∧ x_{2}) ∧ z_{1} ∨ (¬x ∧ x_{1} ∨ x ∧ x_{2}) ∧ z_{2}.

10 This is not the case if the entire abstract function is not needed. In the case of chaotic iteration for example, we can find better encoding of abstract functions.

A Widening Operator on TDGs. The question of the size of a TDG is at the core of efficiency. Of course taking smaller space is efficient in itself, but as seen in section 2, the speed of operators upon a TDG depends directly on its size. To reduce the size we can use less powerful representations without explicit variables and try out different ordering for the variable. So far however, no really satisfactory solution have been brought out, and some cases will always remain exponential for any ordering. So the proposed solution —specific to abstract interpretation— is a widening operator based on the size of the TDG. This widening operator is very general and can be used whenever the size of the abstract domain is too big. In such a case, the encoding of a single element of the abstract domain can be too long for practical manipulation. It is possible by the use of this widening operator to chose an approximate solution that is compact enough for representation on a computer. This widening is quite different from classical widenings used in abstract interpretation as it does not use any semantic information to approximate the result, but only tries to approximate what fills the most space, leaving as much information as possible in the computation framework.

Prerequisites and Characteristics. This widening operator is closely related to the approximation ordering upon P^{♭}, ⪯^{♭} induced by ⪯^{♯}, which should be compatible with the structure of the TDGs. In fact what the widening operator exactly needs is a way to compute the least upper bound of two TDGs for ⪯^{♭}, and, as this operation will be essential to the widening operator, the cheaper the way, the better.

Then, the widening operator takes in a limit size l and a TDG f. The result ▽(l, f) is a TDG g such that |g| ≤ l^{11} and f ⪯^{♭} g. To make sure that it is always possible (for all positive l), we set (+, 1) or (−, 1) as the top of P^{♯}.

This operator can be used to produce a very classical widening operator as defined in the beginning of this section: ▽^{♭}A =^{def} ▽(l(max(A)), max(A)) where max(A) is, if it exists, the maximum of A for the computational ordering^{12} (⊑^{♭}), and l a function that yields the limit.

If the abstract function is coded into TDG too, then this widening operator can be used to do static widening by approximating the abstract function. It can be very profitable because if the TDG used to represent the abstract function is too big, each step of the iteration will be too long, and sometimes the size of the TDG representing the iterates will be directly related to the size of the TDG representing the abstract function. Approximating the abstract function is sound, as justified by the following property:

Property 1 Let F_{1} and F_{2} be monotonic functions (for ⊑). If ∀f F_{1}(f) ⪯ F_{2}(f) and F_{1} or F_{2} are monotonic for ⪯ then

lfp(F_{1}) ⪯ lfp(F_{2})

11 |g| is the number of nodes of g, i.e. its “size” 12 the ordering used to ensure termination of the iterations.

Proof. f ⪯ g implies F_{1}(f) ⪯ F_{2}(g) because F_{1}(f) ⪯ F_{1}(g) by monotonicity and F_{1}(g) ⪯ F_{2}(g) by hypothesis. F_{1}(⊥) ⪯ F_{2}(⊥) by hypothesis. The property follows by induction on the iterates. ⊓ ⊔

Algorithm. The problem is that for this widening operator we will have to find the best possible g such that |g| ≤ l, in a decent amount of time. It is not reasonable to search for the best solution^{13} as it would theoretically require to explore all the possible derivations of a given TDG, which is exponential in the size of the TDG.

Hence we will try to modify the TDG in order to apply one of the reduction steps described in section 2. To obtain sharing, we just consider two nodes of the TDG and, to make them equal, replace them by the least upper bound of the two nodes. To obtain elimination of superfluous nodes, we replace a node N(x, T_{1}, T_{2}) by the least upper bound of T_{1} and T_{2}. Because of the properties required on ⪯^{♭}, this operation gives a TDG greater (for ⪯^{♭}) than the previous one.

The algorithm proceeds by steps: each step, if the size of the TDG is above the limit, try each of the reductions above and take the best one; repeat. The best one is the one with the highest rate

\frac{number of nodes above the limit gained}{cost of the reduction}

where the cost of the reduction is, for a sharing of T_{1} and T_{2}:

cost(T_{1} → T′) × mult(T_{1}) + cost(T_{2} → T′) × mult(T_{2})

and for an elimination of T = N(x, T_{1}, T_{2}):

(cost(T_{1} → T′) + cost(T_{2} → T′)) × mult(T).

Each reduction implies taking the least upper bound T′ of two TDGs T_{1} and T_{2}. The computation of the least upper bound is supposed to yield cost(T_{1} → T′) and cost(T_{2} → T′) ^{14}. Mult is the multiplicity of the node, namely the number of time the node would appear in the Shannon tree representation of the TDG, so that changing a node shared by many would cost more than changing one used by only one.

Each forced reduction will not automatically reduce the size of the TDG because the least upper bound may contain more new nodes than gained through the reduction. However, if the size of the TDG is greater than 1, it will contain a node of the form N(x, (−, 1), (+, 1)). This is because it is the only possible TDG with one variable, so the only possible node in which the greatest (for <^{v}) variable of the TDG appears. So, if (+, 1) or (−, 1) represents the top of P^{♯}, the reduction of this node into the top will always be tried, ensuring that at least

13 That is to say the min (for ⪯^{♭}) of all the possible solutions. 14 This cost is supposed to express the loss of precision; for example it could be the

length of the maximum chain between T_{i} and T′.

one of the modifications tried on the TDG within one step reduces the size of the graph. Thus if the limit is positive the size of the TDG will at each step either decrease or be less than or equal to the limit. Besides, after each step, the new TDG is greater than the previous one for ⪯^{♭}, so the algorithm is correct.

Example Consider the function f = (y ∧ x) ∨ (x ∧ ¬z) ∨ (z ∧ ¬x) defined in the examples of BDDs, with the pointwise ordering for ⪯^{♭} based on 0 ⪯^{♭} 1. See figure 3 for the possible solutions.

[figure: x; −; y; −; y; z; −; 1; x; −; y; −; z; −; 1; y; z; −; 1]

Fig. 3. f and the two best approximates with 3 nodes or less.

Complexity. Considering that at each step, the size of the TDG is reduced by one at least, the number of steps is smaller than the difference between the limit and the size of the TDG. But this is still too much: this difference may be exponential. To reach faster a size closer to the limit, we use a less refined algorithm which assumes that (+, 1) or (−, 1) represents the top. For each node such that the size of the TDG without that node ^{15} lies between the limit and the limit plus half the difference between the limit and the size of the TDG, we try to replace it by the top and take the one that gives the best result. That way, each step of this algorithm at least halves the difference between the limit and the size of the TDG.

The most precise algorithm requires each pair of node to be tested. The multiplicity of each node can be calculated in a time polynomial in the number of nodes by going through the TDG and tagging the nodes. As a result, if the computation of the least upper bound (plus the computation of the costs) is polynomial in the size of the TDGs, then the most precise algorithm is polynomial in the size of the TDG.

Thus we can combine the two algorithms in a way such that if the difference of the size of the TDG and the limit l is bigger than P (l) —where P is a polynomial— then use the rough algorithm else use the other one. Assuming that the limit is polynomial in the number of variables of the TDG, then the global algorithm is polynomial in the number of variables.

15 i.e. after replacing this node by the top.

4 A Complete Example: Strictness Analysis

In this section we describe a complete example of program analysis using abstract interpretation and TDGs. Let’s define first the property to be computed.

Definition 2. A function f is said to be strict in one of its arguments x if everytime the evaluation of that argument fails, the evaluation of f(x) fails

The evaluation fails if it ends with an error or does not terminate.

The goal of a strictness analysis is to determine whether a function is strict in any of its arguments. This can be useful for example in the compilar optimization of a call-by-need prgramming language. The principle of such an implementation is to keep the arguments of functions in a closure until they are first needed in the evaluation of the function and then evaluate them. If a function is strict in an argument then that argument will be always needed, so the compiler can evaluate the argument anyway^{16}, saving in the meantime the space for the closure.

Strictness analysis is a good example of application of TDGs because it is a useful analysis —in a compiler for example— but the most precise abstract interpretations known so far are too slow to be used at higher order.

4.1 Standard Strictness Analysis

What we call standard analysis is the abstract interpretation which will be coded into TDGs. The well-known analysis we use as a basis is one developed by Alan Mycroft in [5], that still seems to be one of the most precise, and that has the advantage of being already coded into boolean functions.

The Concrete Domain. Mycroft’s analysis deals with first order functions from base types to base types. The concrete semantic domain P^{♮} is the set of relations from D to D [19] where D is a complete domain with infimum ⊥ and the values from the base types, such as integers. ⊥^{♮} =^{def} λx.⊥. The concrete semantic function is constructed by induction on the syntax of the expression defining the function: F^{♮} = S[[f(x)=e]].

S[[f(x)=b(e_{1},...,e_{n})]](g) =^{def} \{(x, \underline{b}(v_{1}, …, v_{n}))| ⋀_{1≤i≤n}(x, v_{i}) ∈ S[[f(x)=e_{i}]](g)\}
S[[f(x)=x]](g) =^{def} {(x, x)|x ∈ D}
S[[f(x)=f(e)]](g) =^{def} {(x, w)|(x, v) ∈ S[[f(x)=e]](g) ∧ (v, w) ∈ g}

Where b are constants of the language, such as +, integers or the conditional. \underline{b} is the corresponding constant in P^{♮}. For example \underline{2} = 2, and \underline{cond}(x_{1}, x_{2}, x_{3}) = if x_{1} = ⊥ then ⊥, if x_{1} =true then x_{2} and if x_{1} =false then x_{3}.

16 Assuming there is no side effect.

The Abstract Domain. The abstract domain introduced by Mycroft is the set of monotonic functions from {0, 1} to {0, 1}, with the ordering 0 ⪯^{♯} 1^{17}, which can be interpreted as:

– λx.0 the function never terminates,

– λx.x the function is strict in x and

– λx.1 we do not know.

⊥^{♯} =^{def} λx.0. The abstract semantic function is also defined by induction on the syntax:

S^{♯}[[f(x)=b(e_{1},...,e_{n})]](g^{♯}) =^{def} b^{♯}(S^{♯}[[f(x)=e_{1}]](g^{♯}), …, S^{♯}[[f(x)=e_{n}]](g^{♯}))
S^{♯}[[f(x)=x]](g^{♯}) =^{def} λx.x
S^{♯}[[f(x)=f(e)]](g^{♯}) =^{def} g^{♯} ∘ S^{♯}[[f(x)=e]](g^{♯})

b^{♯} represents b on P^{♯}. For example 2^{♯} = 1 and ite^{♯}(f_{1}, f_{2}, f_{3}) = f_{1} ∧ (f_{2} ∨ f_{3}).

The Relations Between the Two Semantics. The soundness relation between P^{♮} and P^{♯} is described by a Galois connection, P^{♮} \overleftarrow{⟶}^{γ}_{α} P^{♯}:

α(f)(0) =^{def} if {x|(⊥, x) ∈ f} = {⊥} then 0 else 1
α(f)(1) =^{def} if {y|x ∈ D ∧ (x, y) ∈ f} = {⊥} then 0 else 1
γ(λx.0) =^{def} λx.⊥
γ(λx.x) =^{def} {(⊥, ⊥)} ∪ ((D − {⊥}) × D)
γ(λx.1) =^{def} D × D

To ensure that F^{♯} is a good approximation of F we shall make a few more assumptions on the constants:

if ∀i, α(f_{i}) ⪯^{♯} g_{i}^{♯} then

b^{♯}(g_{1}^{♯}, …, g_{n}^{♯}) ⪰^{♯} α(\{(x, \underline{b}(v_{1}, …, v_{n})| ⋀_{1≤i≤n}(x, v_{i}) ∈ f_{i}\})

Then

Property 2 α(lfp(F)) ⪯^{♯} lfp(F^{♯}).

Proof. By induction on the syntax, we shall first prove that ∀f ∈ P^{♮} and ∀g^{♯} ∈ P^{♯}, α(f) ⪯^{♯} g^{♯} implies that α(F (f)) ⪯^{♯} F^{♯}(g^{♯}), then as α(⊥^{♮}) = ⊥^{♯} the inequation on the fixpoints will follow by induction on the iterates.

17 The computational ordering is the same as the approximation ordering.

So let’s suppose α(f) ⪯^{♯} g^{♯}.

α(S[[f(x)=b(e_{1},...,e_{n})]](f))
= α(\{(x, \underline{b}(v_{1}, …, v_{n}))| ⋀_{1≤i≤n}(x, v_{i}) ∈ S[[f(x)=e_{i}]](f)\})
⪯^{♯} b^{♯}(S^{♯}[[f(x)=e_{1}]](g^{♯}), …, S^{♯}[[f(x)=e_{n}]](g^{♯}))
⪯^{♯} S^{♯}[[f(x)=b(e_{1},...,e_{n})]](g^{♯})

The first line is given by definition of S, the second by hypothesis of induction the third by the property of the abstract constants, and finally the fourth by definition of S^{♯}.

α(S[[f(x)=x]](f)) = α({(x, x)|x ∈ D})
= λx.x
= S^{♯}[[f(x)=x]](g^{♯})

For the last step of the proof we need a few more results on the composition of relations. R_{1} ∘ R_{2} =^{def} {(x, w)|(x, v) ∈ R_{2} ∧ (v, w) ∈ R_{1}}. Suppose α(R_{1}) ∘ α(R_{2})(a) = 0. If α(R_{2})(a) = 0 then {y|x ∈ A ∧ (x, y) ∈ R_{2}} = {⊥}^{18} and {y|(⊥, y) ∈ R_{1}} = {⊥}, so {y|x ∈ A ∧ (x, v) ∈ R_{2} ∧ (v, y) ∈ R_{1}} is {⊥}, so α(R_{1} ∘ R_{2})(x) = 0. If α(R_{2})(a) = 1 then {y|(x, y) ∈ R_{1}} = {⊥} so {y|x ∈ A ∧ (x, v) ∈ R_{2} ∧ (v, y) ∈ R_{1}} is {⊥}, so α(R_{1} ∘ R_{2})(x) = 0. It means that ∀R_{i}, α(R_{1} ∘ R_{2}) ⪯^{♯} α(R_{1}) ∘ α(R_{2}).

α(S[[f(x)=f(e)]](f)) = α({(x, w)|(x, v) ∈ S[[f(x)=e]](f) ∧ (v, w) ∈ f})
= α(f ∘ S[[f(x)=e]](f))
⪯^{♯} α(f) ∘ α(S[[f(x)=e]](f))
⪯^{♯} g^{♯} ∘ S^{♯}[[f(x)=e]](g^{♯})
⪯^{♯} S^{♯}[[f(x)=f(e)]](g^{♯})

The first line is the definition of S. Then use the definition of the composition of relations, then what was just proved above on composition and α. The last lines use the fact that α(f) ⪯^{♯} g^{♯} by hypothesis, α(S[[f(x)=e]](f)) ⪯^{♯} S^{♯}[[f(x)=e]](g^{♯}) by hypothesis of induction, and g^{♯} is monotonic as every function in P^{♯}. ⊓ ⊔

It is interesting to notice that Mycroft’s analysis gives more than just the strictness result: it gives results useful in further analysis using this function. For example f(x)=f(x) will give λx.0 so f is strict in x. With the only information that f is strict in x we cannot say that g defined by g(y)=f(0) is also strict.

4.2 The Encoding

To code the abstract domain, we merely add variable names and P^{♭} becomes B_{1}. Abstract functions could be coded using the method presented in the previous

18 If a = 0 then A = {⊥} and if a = 1 then A = D.

section, as they are functions from B_{1} to B_{1}. The problem when dealing with higher order functions is that, since the size of the type is increasing and each step of the iteration requires every possible value of the previous iterate, we will lose all the interest of the TDG for recursive functions. Accordingly we prefer to code each recursive call by a new variable, keeping the arguments of the recursive call. That way, each step of the iteration will only need to make substitutions in the previous iterate, the number of which will be polynomial in the size of the program.

So this abstract interpretation can easily be lifted to higher order functions. As the encoding is very close to the abstract domain, we can have a better build function that associates the boolean function to the set of variables, keeping

only monotonic functions: build{x_{1}, …, x_{2^{n}}} =^{def} λy. ∧ build{x_{1}, …, x_{2^{n−1}}} ∨ y ∧

build{x_{2^{n−1}+1}, …, x_{2^{n}}}.

Given P^{♭} for higher order functions, here is the abstract function:

S^{♭}[[b(e_{1},...,e_{n})]]ρ(g^{♭}) =^{def} b^{♭}(S^{♭}[[e_{1}]]ρ(g^{♭}), …, S^{♭}[[e_{n}]]ρ(g^{♭}))
S^{♭}[[x]]ρ(g^{♭}) =^{def} ρ(x)
S^{♭}[[e_{1}e_{2}]]ρ(g^{♭}) =^{def} S^{♭}[[e_{1}]]ρ(g^{♭})S^{♭}[[e_{2}]]ρ(g^{♭})
S^{♭}[[λx.e]]ρ(g^{♭}) =^{def} S^{♭}[[e]]ρ[x → build(v(x))](g^{♭})

ρ is an environment function. It maps program variables to TDGs. If the variable is associated to a previously analyzed function, it gives the TDG representing the result. If it is a free variable, it gives the TDG as constructed in the previous section representing a variable function, which is, if f is such a function, build(v(f)). We use the type of the variable in order to know what v(f) is, that is to say the exact number of boolean variables needed. If the variable represents the function defined (recursive call), then ρ returns a single boolean variable, and each time it is applied it is replaced by a new variable that will represent the application.

Example:

   s x y z = (x z)(y z)^{19}.

The type of x is α → β → γ, and so it can take at least 2^{4} different values. So we need four boolean variables v(x) = {x_{1}, x_{2}, x_{3}, x_{4}} to represent all the different possible states of x.

ρ(x) = λa.λb.x_{1} ∨ x_{3} ∧ a ∨ (x_{2} ∨ x_{4} ∧ a) ∧ b.

lfp(S^{♭}[[(x z)(y z)]]ρ) is the TDG represented on fig. 4. As, if (x_{1}, x_{2}, x_{3}, x_{4}) = (0, 0, 0, 0), the TDG is 0, s is strict in x. But if x_{1} = 1, the TDG is 1, so the interpretation tells us nothing about the strictness of s in y or z.

The ordering on P^{♭} is the implication, so the max of two TDG is very easy to compute; it is ∧ which is orthogonal. So we can use the widening operator on that example. Moreover, the pointwise ordering on the abstract functions leads to the same ordering (implication) on the representations of the abstract

19 This function is one of the most famous higher ordre functions as with s, k (k x y = x) and i (i x = x), one can code the entire λ-calculus.

[figure: x_{1}; x_{2}; x_{3}; x_{3}; x_{4}; −; y_{1}; y_{1}; y_{1}; y_{2}; −; z; −; 1]

Fig. 4. s x y z = (x z)(y z)

function, so that the same widening can be applied to the abstract set and to the abstract functions.

4.3 Practical Results

Strictness analysis have been implemented using TDGs^{20}, and tested on examples given by Sebastian Hunt to compare the efficiency of this implementation with the one he developed based on ‘frontiers’. All the results below are for the interpreted version (in camllight) and could be improved by compilation. Besides the implementation of Sebastian Hunt was only a prototype implementation, so the comparison might be unfair. However, this results should not be taken as comparable with state of the art strictness analysis, but as an indication of what can be gained using TDGs in program analysis.

n^{o} frontiers TDG
1 10 sec 3 sec
2 5 min  2 sec
3 30 min 4 sec
4 never ended 1 hour

The problems raised by these examples are typical and standard for strictness analysis. The first three examples didn’t require the use of the widening operator, so the results have the same accuracy as with frontiers. The first one is a quite classic nqueen solver, using few higher order functions. The results are quite good with both methods. The second one uses map and foldr^{21}. The third one uses foldr at a higher order, applying it to append, so the result of the analysis is much bigger.

The fourth example analyzes foldr written in continuation passing style, leading to a drastic increase in the type order. Two functions are analyzed with type

(α list → α list → (α list → β) → β) → α list list → α list

→ (α list → β) → β. It is interesting because the result is so huge that it cannot be computed and intermediate results couldn’t be stored by the computer. So it seems to be an example where the TDG representation is exponential that shows the usefulness of the widening presented above. Of course, the result of the analyze is approximate due to the use of this operator.

For the last example, a good alternative to a complete analysis was presented in [23], that gives results in a few seconds. However, this analysis only answers one question and so is not usable for separate compilation. Moreover, the same technique could be applied using TDGs to answer the same question.

5 Conclusion

This approach proved to be efficient in strictness analysis and could be advantageously used in many other abstract interpretations, whatever the context, as its

20 The TDG package used for this implementation is the one developed by Brace,

Rudell and Bryant, as a subset of COSMOS. 21 foldr is the classical function that applies recursively a binary function to a list.

idea is based on the semantic domain not on a fixpoint algorithm. For instance it would work with backward and forward analysis, total or partial fixpoint computation, etc. But the last example shows that it may still be too slow to be usable in practice. This work is totally compatible with the theoretical framework of abstract interpretation, so it could be used in association with other works on this subject. The idea of lazy evaluation of abstract functions from Ferguson and Hughes was mentioned above, but the results of Baraki^{22} on interpretation of polymorphic functions in [22] would be very useful for this approach too, as it could lead to a compact analysis usable in separate analysis. The author believes that the combination of these techniques could give analyzers based on abstract interpretation for higher order functions efficient enough to be usable in practice.

Acknowledgments

I would particularly like to thank Patrick Cousot, for his very heplful advice and support, and for the good idea of using TDGs to represent abstract properties. All the members of his team helped me too with every little problem. The comments from Thomas Jensen were very useful to increase the clarity of this paper. Thanks also to Sebastian Hunt for his very useful examples.

References

1. C. E. Shannon. A Symbolic Analysis of Relay and Switching Circuits. Transactions AIEE, 57:305–316. 1938.

2. P. Cousot & R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. IFIP Conference on Formal Description of Programming Concepts, St-Adrews, N. B., Canada, pp. 237–277. 1977.

3. S. B. Akers. Binary Decision Diagrams. IEEE Transactions on computers. 1978.

4. P. Cousot & R. Cousot. Constructive Version of Tarski’s Fixed Point Theorems. Pacific Journal of Mathematics. 1979.

5. A. Mycroft. The Theory and Practice of Transforming Call-by-Need into Callby-Value.Proceedings of the Fourth International Symposium on Programming, LNCS 83 pp 270–280. 1980.

6. R. E. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comput. C-35, pp. 677–691. 1986.

7. G. L. Burn, C. Hankin & S. Abramsky. Strictness Analysis for Higher-Order Functions. Science of Computer Programming 7, pp. 249–278. 1986.

8. P. Hudak & J. Young. Higher Order Strictness Analysis in Untyped Lambda Calculus. ACM Principles of Programming Languages pp 97–109. 1986.

9. J. P. Billon. Perfect Normal Forms for Discrete Programs. Technical report 87039 BULL. 1987.

10. J. C. Madre & J. P. Billon. Proving Circuit Correctness Using Formal Comparison between Expected and Extracted Behavior. Proc. of the 25th DAC. 1988

11. A. R. Brayton, B. Lin & H. J. Touati. Don’t Care Minimization of Multi-Level Sequential Logic Network. Proc. of ICCAD’90. 1990.

22 He designed a way of using results on polymorphic functions to find the properties of their instantiations 12. J. C. Madre, C. Berthet & O. Coudert. New Ideas in Symbolic Manipulation of

Finite State Machines. Proc. of ICCAD’90. 1990.

13. J. Schwable & K. L. McMillan. Formal Verification of the Encore Gigamax Cache. International Symposium on Shared Memory Multiprocessor. 1991.

14. D. Taubner, E. Enders & T. Filkorn. Generating BDDs for Symbolic Model Checking in CCS. Proc. of CAV’91, pp. 203–213. 1991.

15. H. J. Touati, H. Savoj & R. K. Brayton. Extracting Local Don’t Care for Network Optimization. Proc. of ICCAD’91. 1991.

16. R. E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, Vol. 24. pp. 293–318. 1992.

17. P. Cousot & R. Cousot. Abstract Interpretation Framework. Journal of Logic and Computation, vol 2, No 4, pp. 511–547. 1992.

18. C. Ratel. Définition et réalisation d’un outil de vérification formelle de programmes LUSTRE. Thèse de l’Université de Grenoble 1, chap 11. 1992.

19. P. Cousot & R. Cousot. Galois Connection Based Abstract Interpretations for Strictness Analysis. Proceedings of the International Conference on Formal Methods in Programming and their Applications, LNCS 735 pp 98–127. 1993.

20. B. Le Charlier & P. Van Hentenryck. Groundness Analysis for Prolog: Implementation and Evaluation of the Domain Prop. Proc. of PEPM’93. 1993

21. M.-M. Corsini, M. Musumbu, A. Rauzy & B. Le Charlier Efficient Bottom-up Abstract Interpretation of Logic Programs by means of Constraint Solving. PLILP ’93. 1993.

22. G. Baraki. Abstract Interpretation of Polymorphic Higher-Order Functions. (PhD thesis) Computing Science research report of the University of Glasgow. 1993.

23. A. Ferguson & J. Hughes. Fast Abstract Interpretation Using Sequential Algorithms. Proc. of WSA ’93, pp. 45–59. 1993.

24. P. Van Hentenryck, A. Cortesi & B. Le Charlier. Evaluation of Prop. Journal of Logic Programming. pp 237–278. 1995.