Skip to Main content Skip to Navigation
Conference papers

Constraint solving on modular integers

Arnaud Gotlieb 1 Michel Leconte 2 Bruno Marre 3 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download
Contributor : Arnaud Gotlieb Connect in order to contact the contributor
Submitted on : Monday, May 21, 2012 - 11:18:28 AM
Last modification on : Thursday, January 20, 2022 - 5:33:23 PM
Long-term archiving on: : Wednesday, August 22, 2012 - 2:21:50 AM


Files produced by the author(s)


  • HAL Id : hal-00699234, version 1


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



Record views


Files downloads