Theories, solvers and static analysis by abstract interpretation

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Research output: Contribution to journalArticle

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 languageEnglish (US)
Article number31
JournalJournal of the ACM
Volume59
Issue number6
DOIs
StatePublished - Dec 2012

Fingerprint

Static analysis
Surface mount technology
Semantics
Costs

Keywords

  • Decision procedures
  • Interpretation
  • Program logics
  • Program verification
  • Sat modulo theory
  • Semantics
  • Smt solver
  • Static analysis
  • Theorem proving

ASJC Scopus subject areas

  • Hardware and Architecture
  • Software
  • Artificial Intelligence
  • Information Systems
  • Control and Systems Engineering

Cite this

Theories, solvers and static analysis by abstract interpretation. / Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent.

In: Journal of the ACM, Vol. 59, No. 6, 31, 12.2012.

Research output: Contribution to journalArticle

Cousot, Patrick ; Cousot, Radhia ; Mauborgne, Laurent. / Theories, solvers and static analysis by abstract interpretation. In: Journal of the ACM. 2012 ; Vol. 59, No. 6.
@article{2e5b65cad6cc491399c72a444b621b9a,
title = "Theories, solvers and static analysis by abstract interpretation",
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).",
keywords = "Decision procedures, Interpretation, Program logics, Program verification, Sat modulo theory, Semantics, Smt solver, Static analysis, Theorem proving",
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
year = "2012",
month = "12",
doi = "10.1145/2395116.2395120",
language = "English (US)",
volume = "59",
journal = "Journal of the ACM",
issn = "0004-5411",
publisher = "Association for Computing Machinery (ACM)",
number = "6",

}

TY - JOUR

T1 - Theories, solvers and static analysis by abstract interpretation

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Mauborgne, Laurent

PY - 2012/12

Y1 - 2012/12

N2 - 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).

AB - 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).

KW - Decision procedures

KW - Interpretation

KW - Program logics

KW - Program verification

KW - Sat modulo theory

KW - Semantics

KW - Smt solver

KW - Static analysis

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=84872480610&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84872480610&partnerID=8YFLogxK

U2 - 10.1145/2395116.2395120

DO - 10.1145/2395116.2395120

M3 - Article

VL - 59

JO - Journal of the ACM

JF - Journal of the ACM

SN - 0004-5411

IS - 6

M1 - 31

ER -