DPLL and Abstract Interpretation

Date: Thursday, June 16, 2011
Speaker: Vijay D'Silva
Venue: TU Vienna
Notes:

188/2 – @ 17.00

The DPLL algorithm for deciding propositional satisfiability is a fundamental algorithm with applications across computer science. The modern algorithm combines model search, deduction, and lemma generation in an elegant and highly efficient manner. An important question is whether the DPLL algorithm can be generalised to richer problems such as program verification.

In this talk I show that DPLL operates over a strict abstraction of propositional logic. This is surprising because it uses an imprecise abstraction to obtain precise results. I will show that DPLL very naturally fits in the framework of abstract interpretation. This view leads straight to a generalisation to programs. The application of this algorithm allows complex properties of non-linear programs to be proved automatically using very simple abstractions. Such proofs are well beyond the scope of significantly more mature tools using richer abstractions.

Posted in RiSE Seminar