{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T17:09:20Z","timestamp":1725728960237},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_15","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"215-230","source":"Crossref","is-referenced-by-count":5,"title":["Solving Difference Constraints over Modular Arithmetic"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Gange","sequence":"first","affiliation":[]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"Bj\u00f8rner, N., Blass, A., Gurevich, Y., Musuvathi, M.: Modular difference logic is hard, arXiv:0811.0987v1 (November 2008) (unpublished)"},{"key":"15_CR2","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press (2009)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 179\u2013212. Springer, Heidelberg (1990)"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1145\/367766.368168","volume":"5","author":"R.W. Floyd","year":"1962","unstructured":"Floyd, R.W.: Algorithm 97: Shortest path. Comm. ACM\u00a05, 345 (1962)","journal-title":"Comm. ACM"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"15_CR7","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability. Freeman (1979)"},{"key":"15_CR8","unstructured":"Gotlieb, A., Leconte, M., Marre, B.: Constraint solving on modular integers. In: Proc. Ninth Int. Workshop Constraint Modelling and Reformulation (2010), \n                  \n                    http:\/\/www.it.uu.se\/research\/group\/astra\/ModRef10\/programme.html"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-642-22110-1_39","volume-title":"Computer Aided Verification","author":"A.K. John","year":"2011","unstructured":"John, A.K., Chakraborty, S.: A quantifier elimination algorithm for linear modular equations and disequations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 486\u2013503. Springer, Heidelberg (2011)"},{"key":"15_CR10","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View. Springer (2008)"},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"3","key":"15_CR12","first-page":"321","volume":"7","author":"M. Mohri","year":"2002","unstructured":"Mohri, M.: Semiring frameworks and algorithms for shortest-distance problems. J. Automata, Languages and Combinatorics\u00a07(3), 321\u2013350 (2002)","journal-title":"J. Automata, Languages and Combinatorics"},{"issue":"5","key":"15_CR13","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/1275497.1275504","volume":"29","author":"M. M\u00fcller-Olm","year":"2007","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Programming Languages and Systems\u00a029(5), Article 29 (2007)","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-35182-2_9","volume-title":"Programming Languages and Systems","author":"J.A. Navas","year":"2012","unstructured":"Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Signedness-agnostic program analysis: Precise integer bounds for low-level code. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol.\u00a07705, pp. 115\u2013130. Springer, Heidelberg (2012)"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Regehr, J., Duongsaa, U.: Deriving abstract transfer functions for analyzing embedded software. In: LCTES 2006: Proc. Conf. Language, Compilers, and Tool Support for Embedded Systems, pp. 34\u201343. ACM Press (2006)","DOI":"10.1145\/1134650.1134657"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Sen, R., Srikant, Y.N.: Executable analysis using abstract interpretation with circular linear progressions. In: Proc. Fifth IEEE\/ACM Int. Conf. Formal Methods and Models for Codesign, pp. 39\u201348. IEEE (2007)","DOI":"10.1109\/MEMCOD.2007.371251"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-74061-2_8","volume-title":"Static Analysis","author":"A. Simon","year":"2007","unstructured":"Simon, A., King, A.: Taming the wrapping of integer arithmetic. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 121\u2013136. Springer, Heidelberg (2007)"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 209\u2013222. Springer, Heidelberg (2002)"},{"key":"15_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/11591191_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Wang","year":"2005","unstructured":"Wang, C., Ivan\u010di\u0107, F., Ganai, M.K., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 322\u2013336. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T17:55:31Z","timestamp":1557770131000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}