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
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
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.
Type de document :
Pré-publication, Document de travail
2010
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00543890
Contributeur : Patrick Cousot <>
Soumis le : mardi 7 décembre 2010 - 16:37:00
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : samedi 3 décembre 2016 - 01:13:52

Fichier

LogicalAlgebraicAIreport.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

201

Téléchargements de fichiers

78