A Constraint Solver based on Abstract Domains

Marie Pelleau 1 Antoine Miné 2, 3 Charlotte Truchet 1 Frédéric Benhamou 4
1 TASC - Theory, Algorithms and Systems for Constraints
Inria Rennes – Bretagne Atlantique , Département informatique - EMN, LINA - Laboratoire d'Informatique de Nantes Atlantique
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
3 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
Abstract : In this article, we apply techniques from Abstract Interpretation (a general theory of semantic abstractions) to Constraint Programming (which aims at solving hard combinatorial problems with a generic framework based on first-order logics). We highlight some links and differences between these fields: both compute fixpoints by iteration but employ different extrapolation and refinement strategies; moreover, consistencies in Constraint Programming can be mapped to non-relational abstract domains. We then use these correspondences to build an abstract constraint solver that leverages abstract interpretation techniques (such as relational domains) to go beyond classic solvers. We present encouraging experimental results obtained with our prototype implementation.
Type de document :
Communication dans un congrès
Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 - 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. Springer-Verlag, 7737, pp.434--454, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_26〉
Liste complète des métadonnées

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

https://hal.archives-ouvertes.fr/hal-00785604
Contributeur : Marie Pelleau <>
Soumis le : mercredi 6 février 2013 - 15:00:04
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : samedi 1 avril 2017 - 17:02:19

Fichier

Pelleau_Mine_Truchet_Benhamou....
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou. A Constraint Solver based on Abstract Domains. Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 - 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2013, Rome, Italy. Springer-Verlag, 7737, pp.434--454, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_26〉. 〈hal-00785604〉

Partager

Métriques

Consultations de la notice

841

Téléchargements de fichiers

569