Constraint-based reachability

Arnaud Gotlieb 1 Tristan Denmat 2 Nadjib Lazaar 3
2 LIS - Logical Information Systems
IRISA-D7 - GESTION DES DONNÉES ET DE LA CONNAISSANCE
3 COCONUT - Agents, Apprentissage, Contraintes
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
Abstract : Iterative imperative programs can be considered as infinite-state systems computing over possibly unbounded domains. Studying reachability in these systems is challenging as it requires to deal with an infinite number of states with standard backward or forward exploration strategies. An approach that we call Constraint-based reachability, is proposed to address reachability problems by exploring program states using a constraint model of the whole program. The keypoint of the approach is to interpret imperative constructions such as conditionals, loops, array and memory manipulations with the fundamental notion of constraint over a computational domain. By combining constraint filtering and abstraction techniques, Constraint-based reachability is able to solve reachability problems which are usually outside the scope of backward or forward exploration strategies. This paper pro- poses an interpretation of classical filtering consistencies used in Constraint Programming as abstract domain computations, and shows how this approach can be used to produce a constraint solver that efficiently generates solutions for reachability problems that are unsolvable by other approaches.
Type de document :
Communication dans un congrès
Mohamed Faouzi Atig and Ahmed Rezine. Infinity'2012: 14th International Workshop on Verification of Infinite-State Systems, Aug 2012, Paris, France. pp.19, 2012, 〈http://eptcs.org/content.cgi?Infinity2012〉
Liste complète des métadonnées

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

https://hal-lirmm.ccsd.cnrs.fr/lirmm-00786072
Contributeur : Joël Quinqueton <>
Soumis le : jeudi 7 février 2013 - 16:32:17
Dernière modification le : jeudi 24 mai 2018 - 15:59:23
Document(s) archivé(s) le : mercredi 8 mai 2013 - 03:59:27

Fichier

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

Identifiants

  • HAL Id : lirmm-00786072, version 1

Citation

Arnaud Gotlieb, Tristan Denmat, Nadjib Lazaar. Constraint-based reachability. Mohamed Faouzi Atig and Ahmed Rezine. Infinity'2012: 14th International Workshop on Verification of Infinite-State Systems, Aug 2012, Paris, France. pp.19, 2012, 〈http://eptcs.org/content.cgi?Infinity2012〉. 〈lirmm-00786072〉

Partager

Métriques

Consultations de la notice

460

Téléchargements de fichiers

285