LARA

This is an old revision of the document!

Abstract Interpretation with Conjunctions of Predicates

Parameters: a finite set of formulas ${\cal P} = P_1,\ldots,P_n$ in program variables.

Let $A = 2^{\cal P}$, so for $a \in A$ we have $a \subseteq {\cal P}$

We design analysis using Abstract Interpretation Recipe.

Finite lattice.

Two different orders.