Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00699234
Contributor : Arnaud Gotlieb <>
Submitted on : Monday, May 21, 2012 - 11:18:28 AM
Last modification on : Tuesday, June 15, 2021 - 4:26:30 PM
Long-term archiving on: : Wednesday, August 22, 2012 - 2:21:50 AM

File

GLM_2010_CR.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00699234⟩

Share

Metrics

Record views

546

Files downloads

343