Modular Arithmetic Decision Procedure
[PDF] [PS] [PS.BZ2] [VIEW]
Bibtex:
@techreport{babic-musuvathi-05,
author = {Domagoj Babi\'c and Madanlal Musuvathi},
title = {{Modular Arithmetic Decision Procedure}},
institution = {Microsoft Research Redmond},
year = {2005},
number = {TR-2005-114},
}
Abstract:
All integer data types in programs (such as int, short, byte) have
an underlying finite representation in hardware. This finiteness can
result in subtle integer-overflow errors that are hard to reason about
both for humans and analysis tools alike. As a first step towards
finding such errors automatically, we will describe two modular
arithmetic decision procedures for reasoning about bounded integers.
We show how to deal with modular arithmetic operations and inequalities
for both linear and non-linear problems. Both procedures
are suitable for integration with Nelson-Oppen framework [1, 2, 3].
The linear solver is composed of Müller-Seidl algorithm [4] and an
arbitrary integer solver for solving preprocessed congruences and
inequalities.
For the non-linear problems we use Newton’s p-adic iteration
algorithm to progressively reason about the satisfiability of the input
constraints modulo 2k, for increasing k. We use a SAT solver
only for the base case when k = 1. According to our knowledge,
this is the first Nelson-Oppen decision procedure capable of reasoning
about multiplication over bounded integers without converting
the entire problem to a SAT instance.