TY - GEN
T1 - Solving difference constraints over modular arithmetic
AU - Gange, Graeme
AU - Søndergaard, Harald
AU - Stuckey, Peter J.
AU - Schachte, Peter
PY - 2013/7/15
Y1 - 2013/7/15
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84879966505&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38574-2_15
DO - 10.1007/978-3-642-38574-2_15
M3 - Conference Paper
AN - SCOPUS:84879966505
SN - 9783642385735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 215
EP - 230
BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
PB - Springer
T2 - 24th International Conference on Automated Deduction, CADE 2013
Y2 - 9 June 2013 through 14 June 2013
ER -