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
Is it the case that ?
Using a theorem prover to compute .