Abstract Interpretation as Automated Deduction
Venue
Automated Deduction - CADE 25, Springer International Publishing (2015), pp. 450-464
Publication Year
2015
Authors
Vijay D'Silva, Caterina Urban
BibTeX
Abstract
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.
