Solving difference constraints over modular arithmetic

Graeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

4 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationCADE 2013 - 24th International Conference on Automated Deduction, Proceedings
PublisherSpringer
Pages215-230
Number of pages16
ISBN (Print)9783642385735
DOIs
Publication statusPublished - 15 Jul 2013
Externally publishedYes
Event24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, United States of America
Duration: 9 Jun 201314 Jun 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7898 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Automated Deduction, CADE 2013
Country/TerritoryUnited States of America
CityLake Placid
Period9/06/1314/06/13

Cite this