Constraint solving on modular integers

Abstract : Constraint solving over nite-sized integers involves the def- inition of propagators able to capture modular (a.k.a. wrap-around) in- teger computations. In this paper, we propose e cient propagators for a fragment of modular integer constraints including adders, multipliers and comparators. Our approach is based on the original notion of Clock- wise Interval for which we de ne a complete arithmetic. We also present three distinct implementations of modular integer constraint solving in the context of software verification.
Type de document :
Communication dans un congrès
ModRef Worksop, associated to CP'2010, Sep 2010, Saint-Andrews, United Kingdom. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00699234
Contributeur : Arnaud Gotlieb <>
Soumis le : lundi 21 mai 2012 - 11:18:28
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : mercredi 22 août 2012 - 02:21:50

Fichier

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

Identifiants

  • HAL Id : hal-00699234, version 1

Citation

Arnaud Gotlieb, Michel Leconte, Bruno Marre. Constraint solving on modular integers. ModRef Worksop, associated to CP'2010, Sep 2010, Saint-Andrews, United Kingdom. 2010. 〈hal-00699234〉

Partager

Métriques

Consultations de la notice

460

Téléchargements de fichiers

201