{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T18:45:16Z","timestamp":1747853116181,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_11","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"171-186","source":"Crossref","is-referenced-by-count":17,"title":["Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods"],"prefix":"10.1007","author":[{"given":"Vijay","family":"Ganesh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergey","family":"Berezin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Tod Amon, Gaetano Borriello, Taokuan Hu, and Jiwen Liu. Symbolic timing verification of timing diagrams using Presburger formulas. In Design Automation Conference, pages 226\u2013231, 1997.","DOI":"10.1145\/266021.266071"},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Colloquium on Trees in Algebra and Programming (CAAP\u201996)","author":"A. Boudet","year":"1996","unstructured":"Alexandre Boudet and Hubert Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Colloquium on Trees in Algebra and Programming (CAAP\u201996), volume 1059 of Lecture Notes in Computer Science, pages 30\u201343. Springer Verlag, 1996."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"R. Brinkmann and R. Drechsler. RTL-datapath verification using integer linear programming. InIEEEVLSIDesign\u201901 & Asia and South Pacific Design Automation Conference, Bangalore, pages 741\u2013746, 2002.","DOI":"10.1109\/ASPDAC.2002.995022"},{"issue":"8","key":"11_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. R. B\u00fcchi","year":"1960","unstructured":"J. R. B\u00fcchi. Weak second-order arithmetic and finite automata. Zeitschrift f\u00fcr mathematische Logik und Grundladen der Mathematik, 6:66\u201392, 1960.","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundladen der Mathematik"},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98:142\u2013170, 1992.","journal-title":"Information and Computation"},{"issue":"2","key":"11_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR8","first-page":"91","volume":"7","author":"D. C. Cooper","year":"1972","unstructured":"D. C. Cooper. Theorem proving in arithmetic without multiplication. In Machine Intelligence, volume 7, pages 91\u201399, New York, 1972. American Elsevier.","journal-title":"Machine Intelligence"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G. B. Dantzig","year":"1973","unstructured":"George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14:288\u2013297, 1973.","journal-title":"Journal of Combinatorial Theory (A)"},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification, CAV\u2019 98, Proceedings","author":"J. Elgaard","year":"1998","unstructured":"Jacob Elgaard, Nils Klarlund, and Anders M\u00f8ller. Mona 1.x: new techniques for ws1s and ws2s. In Computer Aided Verification, CAV\u2019 98, Proceedings, volume 1427 of LNCS. Springer Verlag, 1998."},{"key":"11_CR11","unstructured":"P. Johannsen and R. Drechsler. Formal verification on the RT level computing one-to-one design abstractions by signal width reduction. In IFIP International Conference on Very Large Scale Integration (VLSI\u201901), Montpellier, 2001, pages 127\u2013132, 2001."},{"key":"11_CR12","unstructured":"G. Kreisel and J. Krivine. Elements of mathematical logic, 1967."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Derek C. Oppen. A 222pn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16(3):323\u2013332, June 1978.","DOI":"10.1016\/0022-0000(78)90021-1"},{"key":"11_CR15","unstructured":"M. Presburger. Uber de vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves, pages 92\u2013101, 395, Warsaw, 1927."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"William Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Supercomputing, pages 4\u201313, 1991.","DOI":"10.1145\/125826.125848"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In A. J. Hu and M. Y. Vardi, editors, Proceedings of the 10th International Conference on Computer Aided Verification, volume 1427, pages 280\u2013292. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0028752"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1016\/0097-3165(76)90055-8","volume":"21","author":"H. P. Williams","year":"1976","unstructured":"H. P. Williams. Fourier-Motzkin elimination extension to integer programming problems. Journal of Combinatorial Theory (A), 21:118\u2013123, 1976.","journal-title":"Journal of Combinatorial Theory (A)"},{"key":"11_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Pierre Wolper and Bernard Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 1\u201319, Berlin, March 2000. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:24:43Z","timestamp":1739993083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}