{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:10:26Z","timestamp":1771024226639,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540646082","type":"print"},{"value":"9783540693390","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028752","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"280-292","source":"Crossref","is-referenced-by-count":21,"title":["A comparison of Presburger engines for EFSM reachability"],"prefix":"10.1007","author":[{"given":"Thomas R.","family":"Shiple","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James H.","family":"Kukula","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev K.","family":"Ranjan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"T. Amon, G. Bordello, T Hu, and J. Liu. Symbolic timing verification of timing diagrams using Presburger formulas. In Proc. 34th Design Automat. Conf., pages 226\u2013237, June 1997.","DOI":"10.1145\/266021.266071"},{"key":"27_CR2","series-title":"volume 1135 of LNCS","volume-title":"Fourth International Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M. Biehl","year":"1996","unstructured":"M. Biehl, N. Klarlund, and T. Rauhe. Mona: Decidable arithmetic in practice. In B. Jonsson and J. Parrow, editors, Fourth International Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of LNCS, Uppsala, Sweden, 1996. Springer-Verlag."},{"key":"27_CR3","series-title":"volume 818 of LNCS","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/3-540-58179-0_43","volume-title":"Proc. Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In D. L. Dill, editor, Proc. Computer Aided Verification, volume 818 of LNCS, pages 55\u201367, Stanford, CA, June 1994. Springer-Verlag."},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"A. Boudet and H. Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Trees and Algebra in Programming-CAAP, volume 1059 of LNCS, pages 30\u201343. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61064-2_27"},{"key":"27_CR5","series-title":"volume 1102 of LNCS","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proceedings of the Conference on Computer-Aided Verification","author":"R. K. Brayton","year":"1996","unstructured":"R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In R. Alur and T. A. Henzinger, editors, Proceedings of the Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 428\u2013432, New Brunswick, NJ, July 1996. Springer-Verlag."},{"key":"27_CR6","first-page":"1","volume-title":"Proc. Int. Congress Logic, Methodology, and Philosophy of Science","author":"J. R. B\u00fcchi","year":"1960","unstructured":"J. R. B\u00fcchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congress Logic, Methodology, and Philosophy of Science, pages 1\u201311, Berkeley, CA, 1960. Stanford University Press."},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Bultan, R. Gerber, and C. League. Verifying systems with integer constraints and boolean predicates: A composite approach. In Proceedings of the 1998 International Symposium on Software Testing and Analysis (ISSTA '98), 1998.","DOI":"10.1145\/271771.271799"},{"key":"27_CR8","series-title":"volume 1254 of LNCS","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Proc. Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic model checking of infinite state programs using Presburger arithmetic. In O. Grumberg, editor, Proc. Computer Aided Verification, volume 1254 of LNCS, pages 400\u2013411, Haifa, June 1997. Springer-Verlag."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"K.-T Cheng and A. Krishnakumar. Automatic functional test generation using the extended finite state machine model. In Proc. 30th Design Automat. Conf., pages 86\u201391, June 1993.","DOI":"10.1145\/157485.164585"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 365\u2013373. Springer-Verlag, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"issue":"5","key":"27_CR11","doi-asserted-by":"publisher","first-page":"722","DOI":"10.1109\/43.277617","volume":"12","author":"S. Devadas","year":"1993","unstructured":"S. Devadas. Comparing two-level and ordered binary decision diagram representations of logic functions. IEEE Trans. Computer-Aided Design, 12(5):722\u2013723, May 1993.","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"S. Devadas, K. Keutzer, and A. Krishnakumar. Design verification and reachability analysis using algebraic manipulation. In Proc. Int'l Conf. on Computer Design, pages 250\u2013258, Oct. 1991.","DOI":"10.1109\/ICCD.1991.139892"},{"key":"27_CR13","volume-title":"A Mathematical Introduction to Logic","author":"H. B. Enderton","year":"1972","unstructured":"H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, New York, 1972."},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"J. G. Henriksen, J. Jensen, M. J\u00f8rgensen, N. Klarlund, R. Paige, T Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95, volume 1019 of LNCS, pages 89\u2013110. Springer-Verlag, May 1995.","DOI":"10.1007\/3-540-60630-0_5"},{"key":"27_CR15","unstructured":"W. Kelly, V. Maslov, W. Pugh, E. Rosser, T Shpeisman, and D. Wonnacott. The Omega library (Version 1.1.0) interface guide. http:\/\/www.cs.umd.edu\/ projects\/omega, Nov. 1996."},{"issue":"3","key":"27_CR16","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D. Oppen","year":"1978","unstructured":"D. Oppen. A $$2^{2^{2^{pn} } }$$ upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16(3):323\u2013332, July 1978.","journal-title":"Journal of Computer and System Sciences"},{"issue":"8","key":"27_CR17","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102\u2013114, Aug. 1992.","journal-title":"Communications of the ACM"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"B. L. van der Waerden. Modern Algebra, volume 1. Ungar, 1953.","DOI":"10.1007\/978-1-4684-9999-5_1"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"P Wolper and B. Boigelot. An automata-theoretic approach to Presburger arithmetic constraints. In Proc. of Static Analysis Symposium, volume 983 of LNCS, pages 21\u201332. Springer-Verlag, Sept. 1995.","DOI":"10.1007\/3-540-60360-3_30"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028752","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:23:47Z","timestamp":1586593427000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028752"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0028752","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}