Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s10817-016-9382-4 | J. Autom. Reasoning |
Keywords | Field | DocType |
Abstract interpretation,Deduction,Lindenbaum–Tarski construction | Local consistency,Parameterized complexity,Abstract interpretation,Computer science,Automated theorem proving,Satisfiability,Algorithm,Reachability,Theoretical computer science,Parametric statistics,Monad (functional programming) | Conference |
Volume | Issue | ISSN |
58 | 3 | 0168-7433 |
Citations | PageRank | References |
3 | 0.40 | 28 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vijay D'Silva | 1 | 239 | 14.07 |
| Caterina Urban | 2 | 79 | 5.39 |