Constraint-based reachability - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Constraint-based reachability

Résumé

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 {\it 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 {\it constraint} over a computational domain. By combining constraint filtering and abstraction techniques, {\it Constraint-based reachability} is able to solve reachability problems which are usually outside the scope of backward or forward exploration strategies. This paper proposes 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.
Fichier principal
Vignette du fichier
GotliebDenmatLazaar_Infinity2012201302070156.pdf (160.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00807856 , version 1 (04-04-2013)

Identifiants

Citer

Arnaud Gotlieb, Tristan Denmat, Nadjib Lazaar. Constraint-based reachability. Infinity workshop 2012, Aug 2012, Paris, France. ⟨10.4204/EPTCS.107.4⟩. ⟨hal-00807856⟩
883 Consultations
361 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More