The reduced product of abstract domains and the combination of decision procedures

Patrick Cousot, Radhia Cousot, Laurent Mauborgne

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses 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). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.

Original languageEnglish (US)
Title of host publicationFoundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings
Pages456-472
Number of pages17
Volume6604 LNCS
DOIs
StatePublished - 2011
Event14th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 - Saarbrucken, Germany
Duration: Mar 26 2010Apr 3 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6604 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
CountryGermany
CitySaarbrucken
Period3/26/104/3/10

Fingerprint

Decision Procedures
Surface mount technology
Static analysis
Transformer
Semantics
Static Analysis
Soundness
Convexity
Costs
Completeness
Equality
Restriction
Term
Observation
Abstraction
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cousot, P., Cousot, R., & Mauborgne, L. (2011). The reduced product of abstract domains and the combination of decision procedures. In Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings (Vol. 6604 LNCS, pp. 456-472). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6604 LNCS). https://doi.org/10.1007/978-3-642-19805-2_31

The reduced product of abstract domains and the combination of decision procedures. / Cousot, Patrick; Cousot, Radhia; Mauborgne, Laurent.

Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. Vol. 6604 LNCS 2011. p. 456-472 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6604 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P, Cousot, R & Mauborgne, L 2011, The reduced product of abstract domains and the combination of decision procedures. in Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. vol. 6604 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6604 LNCS, pp. 456-472, 14th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrucken, Germany, 3/26/10. https://doi.org/10.1007/978-3-642-19805-2_31
Cousot P, Cousot R, Mauborgne L. The reduced product of abstract domains and the combination of decision procedures. In Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. Vol. 6604 LNCS. 2011. p. 456-472. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-19805-2_31
Cousot, Patrick ; Cousot, Radhia ; Mauborgne, Laurent. / The reduced product of abstract domains and the combination of decision procedures. Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. Vol. 6604 LNCS 2011. pp. 456-472 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5ed4eb19607246939f64b9c16e16bb12,
title = "The reduced product of abstract domains and the combination of decision procedures",
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 and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses 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). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.",
author = "Patrick Cousot and Radhia Cousot and Laurent Mauborgne",
year = "2011",
doi = "10.1007/978-3-642-19805-2_31",
language = "English (US)",
isbn = "9783642198045",
volume = "6604 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "456--472",
booktitle = "Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings",

}

TY - GEN

T1 - The reduced product of abstract domains and the combination of decision procedures

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Mauborgne, Laurent

PY - 2011

Y1 - 2011

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 and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses 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). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.

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 and computation on-the-fly of property transformers. It is very expressive. We propose a combination of the two approaches to reach the sweet spot best adapted to a specific application domain in the precision/cost spectrum. The proposed combination uses 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). We also introduce a semantics based on multiple interpretations to deal with the soundness of that combinations on a formal basis.

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

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

U2 - 10.1007/978-3-642-19805-2_31

DO - 10.1007/978-3-642-19805-2_31

M3 - Conference contribution

SN - 9783642198045

VL - 6604 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 456

EP - 472

BT - Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings

ER -