Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.
CITATION STYLE
Kafle, B., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2017). A benders decomposition approach to deciding modular linear integer arithmetic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10491 LNCS, pp. 380–397). Springer Verlag. https://doi.org/10.1007/978-3-319-66263-3_24
Mendeley helps you to discover research relevant for your work.