Abstract Interpretation as Automated Deduction |
| |
Authors: | Vijay D’Silva Caterina Urban |
| |
Affiliation: | 1.Google Inc.,San Francisco,USA;2.ETH Zürich,Zürich,Switzerland |
| |
Abstract: | Automata theory, algorithmic deduction and abstract interpretation provide the foundation behind three approaches to implementing program verifiers. This article is a first step towards a mathematical translation between these approaches. By extending Büchi’s theorem, we show that reachability in a control flow graph can be encoded as satisfiability in an extension of the weak, monadic, second-order logic of one successor. Abstract interpreters are, in a precise sense, sound but incomplete solvers for such formulae. The three components of an abstract interpreter: the lattice, transformers and iteration algorithm, respectively represent a fragment of a first-order theory, deduction in that theory, and second-order constraint propagation. By inverting the Lindenbaum–Tarski construction, we show that lattices used in practice are subclassical first-order theories. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|