Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Framework for Combining Algebraic and Logical Abstract Interpretations

Patrick Cousot 1, 2 Radhia Cousot 1, 2 Laurent Mauborgne 2, 3 
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique - ENS Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : We introduce a reduced product combining algebraic and logical abstractions to design program correctness verifiers and static analyzers by abstract interpretation. The key new idea is to show that the Nelson-Oppen procedure for combining theories in SMT-solvers computes a reduced product in an observational semantics, so that algebraic and logical abstract interpretations can naturally be combined in a classical way using a reduced product on this observational semantics. The main practical benefit is that reductions can be performed within the logical abstract domains, within the algebraic abstract domains, and also between the logical and the algebraic abstract domains, including the case of abstractions evolving during the analysis.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [33 references]  Display  Hide  Download

https://hal.inria.fr/inria-00543890
Contributor : Patrick Cousot Connect in order to contact the contributor
Submitted on : Tuesday, December 7, 2010 - 4:37:00 PM
Last modification on : Thursday, March 17, 2022 - 10:08:36 AM
Long-term archiving on: : Saturday, December 3, 2016 - 1:13:52 AM

File

LogicalAlgebraicAIreport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00543890, version 1

Collections

Citation

Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Framework for Combining Algebraic and Logical Abstract Interpretations. 2010. ⟨inria-00543890⟩

Share

Metrics

Record views

114

Files downloads

60