Tue May 13, 2008, 2:00-3:50, 5272 Boelter Hall (part 1)
Thu May 15, 2008, 2:00-3:50, 5272 Boelter Hall (part 2)
Logical Abstract Interpretation
Sumit Gulwani
Microsoft Research
Logical Abstract Interpretation means performing abstract interpretation
over abstract domains whose elements are logical formulas over some theory
and the partial order relationship is the implication relationship
(or some refinement of it). Theorem proving community has studied decision
procedures for several theories. For performing abstract interpretation
over logical formulas in a theory, we need more than a decision procedure.
In particular, we need a join operator that can over-approximation
disjunction, a postcondition operator that over-approximates existential
quantifier elimination, a widen operator that guarantees convergence during
the fixed-point computation process. In this project, we have shown how to
build such transfer functions for a theory taking inspiration from the
decision procedure for that theory. Of these, the join algorithm is
typically the tricky part.
We have described logical abstract interpretation for the theory of
uninterpreted functions. The decision procedure for this theory consists
of performing the classic congruence closure over a data-structure
called EDAG (Equivalence DAG). The join algorithm involves performing
intersection of (the congurence classes of) two EDAGs. We used these
transfer functions to describe the first PTIME algorithm for the classic
problem of global value numbering.
We have also described logical abstract interpretation for combination of
two theories (such as the combined theory of linear arithmetic and
uninterpreted functions) given the logical abstract interpreter for
constituent theories. The decision procedure for this theory consists
of using the classic Nelson Oppen methodology for combining
decision procedures. The join algorithm is more involved and
requires adding some new definitions before performing join in the
constituent theories.
We have also described logical abstract interpretation for universally
quantified formulas over some base theory given a logical abstract
interpreter for the base theory. This requires development of
under-approximation algorithms for base theories.
About the speaker: Sumit Gulwani's research interests are primarily in
the area of program analysis and verification. His work has drawn on
techniques from randomized algorithms, theorem proving, model checking,
and machine learning. He obtained his Phd in Computer Science from
UC Berkeley in 2005, and his BTech degree in Computer Science and
Engineering from IIT Kanpur in 2000.
Host: Jens Palsberg