This is an old revision of the document!
Abstract Interpretation with Conjunctions of Predicates
Parameters: a finite set of formulas in program variables. Suppose is the predicate 'false'.
Let , so for we have .
We design analysis using Abstract Interpretation Recipe.
Define a syntactic order on
Finite lattice.
Defining .
Defining .
Is it the case that ?