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.

for $a \in A$ we have $a \subseteq {\cal P}$

Using Abstract Interpretation Recipe we construct:

  • abstract domain: truth values of predicates
  • concretization function: states given by truth values
  • abstraction function
  • best abstract post for simple programming language

Finite lattice.

Two different orders.