Modular Arithmetic Decision Procedure

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 Muller-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 2, 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.