 |
    |
Solving Difference Constraints over Modular Arithmetic
Graeme Gange, Harald Søndergaard, Peter J. Stuckey, and Peter Schachte
Department of Computing and Information Systems, The University of Melbourne, Victoria 3010, Australiaggange@csse.unimelb.edu.au
harald@csse.unimelb.edu.au
pjs@csse.unimelb.edu.au
schachte@csse.unimelb.edu.au
Abstract. Difference logic is commonly used in program verification and analysis. In the context of fixed-precision integers, as used in assembly languages for example, the use of classical difference logic is unsound. We study the problem of deciding difference constraints in the context of modular arithmetic and show that it is strongly NP-complete. We discuss the applicability of the Bellman-Ford algorithm and related shortest-distance algorithms to the context of modular arithmetic. We explore two approaches, namely a complete method implemented using SMT technology and an incomplete fixpoint-based method, and the two are experimentally evaluated. The incomplete method performs considerably faster while maintaining acceptable accuracy on a range of instances.
LNAI 7898, p. 215 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013