Abstract
The algebraic/model theoretic design of static analyzers uses abstract domains based on representations of properties and pre-calculated property transformers. It is very efficient. The logical/proof theoretic approach uses SMT solvers/theorem provers and computation of property transformers on-the-fly. It is very expressive. We propose to unify both approaches, so that they can be combined to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. We first give a new formalization of the proof theoretic approach in the abstract interpretation framework, introducing a semantics based on multiple interpretations to deal with the soundness of such approaches. Then we describe how to combine them with any other abstract interpretation-based analysis using an iterated reduction to combine abstractions. The key observation is that the Nelson-Oppen procedure, which decides satisfiability in a combination of logical theories by exchanging equalities and disequalities, computes a reduced product (after the state is enhanced with some new "observations" corresponding to alien terms). By abandoning restrictions ensuring completeness (such as disjointness, convexity, stably-infiniteness, or shininess, etc.), we can even broaden the application scope of logical abstractions for static analysis (which is incomplete anyway).
Original language | English (US) |
---|---|
Article number | 31 |
Journal | Journal of the ACM |
Volume | 59 |
Issue number | 6 |
DOIs | |
State | Published - Dec 2012 |
Keywords
- Decision procedures
- Interpretation
- Program logics
- Program verification
- Sat modulo theory
- Semantics
- Smt solver
- Static analysis
- Theorem proving
ASJC Scopus subject areas
- Software
- Control and Systems Engineering
- Information Systems
- Hardware and Architecture
- Artificial Intelligence