Friday, August 14, 2015
Speaker: Caterina Urban
Venue: TU Wien
Time: 9:00, Day:Friday
Algorithmic deduction and abstract interpretation are two widely used
and successful approaches to implementing program verifiers. A major
impediment to combining these approaches is that their mathematical
foundations and implementation approaches are fundamentally different.
This paper presents a new, logical perspective on abstract
interpreters that perform reachability analysis using non-relational
domains. We encode reachability of a location in a control-flow graph
as satisfiability in a monadic, second-order logic parameterized by a
first-order theory. We show that three components of an abstract
interpreter, the lattice, transformers and iteration algorithm,
represent a first-order, substructural theory, parametric deduction
and abduction in that theory, and second-order constraint propagation.