Abstract Interpretation as Automated Deduction

Vijay d'Silva (1) , Caterina Urban (2)

1 Google Inc [Mountain View]
2 DI-ENS - Département d'informatique - ENS Paris

Algorithmic deduction and abstract interpretation are two widely used and successful approaches to implementing program veri-fiers. 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.

Domaines: Logique en informatique [cs.LO]

Vijay d'Silva, Caterina Urban. Abstract Interpretation as Automated Deduction. 25th International Conference on Automated Deduction (CADE 2015), 2015, Berlin, Germany. ⟨hal-01952896⟩