@InProceedings{Gan-Son-Stu-Sch_CADE13,
  author    = {Graeme Gange and 
		Harald S{\o}ndergaard and 
		Peter J. Stuckey and 
		Peter Schachte},
  title     = {Solving Difference Constraints over Modular Arithmetic},
  editor    = {M. P. Bonacina},
  booktitle = {CADE 2013: Proceedings of the 24th International
		Conference on Automated Deduction},
  series    = {Lecture Notes in Artificial Intelligence},
  volume    = {7898},
  pages     = {215--230},
  publisher = {Springer},
  year      = {2013},
  doi       = {10.1007/978-3-642-38574-2_15},
  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.},
  keywords  = {Constraint solving, Program verification, Static analysis, Machine arithmetic, Fixed points},
}

{"_id":"uek2WcuMC4hyf7exa","bibbaseid":"gange-sndergaard-stuckey-schachte-solvingdifferenceconstraintsovermodulararithmetic-2013","author_short":["Gange, G.","Søndergaard, H.","Stuckey, P. J.","Schachte, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"firstnames":["Graeme"],"propositions":[],"lastnames":["Gange"],"suffixes":[]},{"firstnames":["Harald"],"propositions":[],"lastnames":["Søndergaard"],"suffixes":[]},{"firstnames":["Peter","J."],"propositions":[],"lastnames":["Stuckey"],"suffixes":[]},{"firstnames":["Peter"],"propositions":[],"lastnames":["Schachte"],"suffixes":[]}],"title":"Solving Difference Constraints over Modular Arithmetic","editor":[{"firstnames":["M.","P."],"propositions":[],"lastnames":["Bonacina"],"suffixes":[]}],"booktitle":"CADE 2013: Proceedings of the 24th International Conference on Automated Deduction","series":"Lecture Notes in Artificial Intelligence","volume":"7898","pages":"215–230","publisher":"Springer","year":"2013","doi":"10.1007/978-3-642-38574-2_15","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.","keywords":"Constraint solving, Program verification, Static analysis, Machine arithmetic, Fixed points","bibtex":"@InProceedings{Gan-Son-Stu-Sch_CADE13,\n author = {Graeme Gange and \n\t\tHarald S{\\o}ndergaard and \n\t\tPeter J. Stuckey and \n\t\tPeter Schachte},\n title = {Solving Difference Constraints over Modular Arithmetic},\n editor = {M. P. Bonacina},\n booktitle = {CADE 2013: Proceedings of the 24th International\n\t\tConference on Automated Deduction},\n series = {Lecture Notes in Artificial Intelligence},\n volume = {7898},\n pages = {215--230},\n publisher = {Springer},\n year = {2013},\n doi = {10.1007/978-3-642-38574-2_15},\n abstract = {Difference logic is commonly used in program verification \n\t\tand analysis. In the context of fixed-precision integers,\n\t\tas used in assembly languages for example, the use of \n\t\tclassical difference logic is unsound. We study the problem\n\t\tof deciding difference constraints in the context of modular\n\t\tarithmetic and show that it is strongly NP-complete. We \n\t\tdiscuss the applicability of the Bellman-Ford algorithm and \n\t\trelated shortest-distance algorithms to the context of modular\n\t\tarithmetic. We explore two approaches, namely a complete \n\t\tmethod implemented using SMT technology and an incomplete \n\t\tfixpoint-based method, and the two are experimentally \n\t\tevaluated. The incomplete method performs considerably \n\t\tfaster while maintaining acceptable accuracy on a range\n\t\tof instances.},\n keywords = {Constraint solving, Program verification, Static analysis, Machine arithmetic, Fixed points},\n}\n\n","author_short":["Gange, G.","Søndergaard, H.","Stuckey, P. J.","Schachte, P."],"editor_short":["Bonacina, M. P."],"key":"Gan-Son-Stu-Sch_CADE13","id":"Gan-Son-Stu-Sch_CADE13","bibbaseid":"gange-sndergaard-stuckey-schachte-solvingdifferenceconstraintsovermodulararithmetic-2013","role":"author","urls":{},"keyword":["Constraint solving","Program verification","Static analysis","Machine arithmetic","Fixed points"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"people.eng.unimelb.edu.au/harald/bibbase.bib","dataSources":["yWvm3kzg5vKQAPLm7","ofmsZryxNDBSpE7j5","9aC4cxLD8D6oJ3FLN","wpkuJrZJJtqra3FbL","XqcrNTrCCBr9mSd37","W7ih7WyQivP4EDh83"],"keywords":["constraint solving","program verification","static analysis","machine arithmetic","fixed points"],"search_terms":["solving","difference","constraints","over","modular","arithmetic","gange","søndergaard","stuckey","schachte"],"title":"Solving Difference Constraints over Modular Arithmetic","year":2013}