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