Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-38574-2_15 | CADE |
Keywords | Field | DocType |
bellman-ford algorithm,incomplete method,classical difference logic,smt technology,acceptable accuracy,complete method,difference constraint,difference logic,modular arithmetic,incomplete fixpoint-based method | Integer,Discrete mathematics,Separation logic,Complete Method,Modular arithmetic,Computer science,Algorithm,Theoretical computer science,Assembly language,Fixed point | Conference |
Citations | PageRank | References |
5 | 0.41 | 17 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Graeme Gange | 1 | 137 | 24.27 |
| Harald Søndergaard | 2 | 858 | 79.52 |
| Peter J. Stuckey | 3 | 4368 | 457.58 |
| Peter Schachte | 4 | 256 | 22.76 |