{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:57:40Z","timestamp":1725512260264},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540708889"},{"type":"electronic","value":"9783540708896"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70889-6_5","type":"book-chapter","created":{"date-parts":[[2007,5,10]],"date-time":"2007-05-10T14:04:16Z","timestamp":1178805856000},"page":"65-80","source":"Crossref","is-referenced-by-count":3,"title":["Verification of Data Paths Using Unbounded Integers: Automata Strike Back"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Schuele","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Leja, F. (ed.): Sprawozdanie z I Kongresu Matematyk\u00f3w Kraj\u00f3w S\u0142owia\u0144skich, Warszawa, 1929 (Comptes\u2013rendus du I Congr\u00e9s des Math\u00e9maticiens des Pays Slaves, Varsovie 1929), Warszawa, pp. 92\u2013101 (supplement on p. 395) (1929)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S.K. Lahiri","year":"2002","unstructured":"Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 142\u2013159. Springer, Heidelberg (2002)"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"J. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.: Weak second order arithmetic and finite automata. Z. Math. Logik Grundlagen Math.\u00a06, 66\u201392 (1960)","journal-title":"Z. Math. Logik Grundlagen Math."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Klaedtke, F.: On the automata size for Presburger arithmetic. Technical Report 186, Institute of Computer Science at Freiburg University (2003)","DOI":"10.1109\/LICS.2004.1319605"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/3-540-36126-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"V. Ganesh","year":"2002","unstructured":"Ganesh, V., Berezin, S., Dill, D.L.: Deciding Presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 171\u2013186. Springer, Heidelberg (2002)"},{"issue":"2:6","key":"5_CR8","first-page":"1","volume":"1","author":"S.A. Seshia","year":"2005","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. Logical Methods in Computer Science\u00a01(2:6), 1\u201326 (2005)","journal-title":"Logical Methods in Computer Science"},{"key":"5_CR9","unstructured":"Boigelot, B.: The Li\u00e8ge automata-based symbolic handler (LASH) (2006), http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"5_CR10","unstructured":"Janicic, P., Green, I., Bundy, A.: A comparison of decision procedures in Presburger arithmetic. Research Paper 872, University of Edinburgh (1997)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/BFb0028752","volume-title":"Computer Aided Verification","author":"T.R. Shiple","year":"1998","unstructured":"Shiple, T.R., Kukula, J.H., Ranjan, R.K.: A comparison of Presburger engines for EFSM reachability. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 280\u2013292. Springer, Heidelberg (1998)"},{"key":"5_CR12","first-page":"229","volume-title":"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, T\u00fcbingen, Germany, GI\/ITG\/GMM","author":"T. Schuele","year":"2002","unstructured":"Schuele, T., Schneider, K.: Symbolic model checking by automata based set representation. In: Ruf, J. (ed.) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, T\u00fcbingen, Germany, GI\/ITG\/GMM, pp. 229\u2013238. Shaker, Aachen (2002)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-36126-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Strichman","year":"2002","unstructured":"Strichman, O.: On solving Presburger and linear arithmetic with SAT. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 160\u2013170. Springer, Heidelberg (2002)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., et al.: Abstraction-based satisfiability solving of Presburger arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-3-642-59136-5_2","volume-title":"Handbook of Formal Languages, vol. 1","author":"S. Yu","year":"1997","unstructured":"Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41\u2013110. Springer, Heidelberg (1997)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1080\/00207169008803893","volume":"35","author":"A. Fellah","year":"1990","unstructured":"Fellah, A., J\u00fcrgensen, H., Yu, S.: Constructions for alternating finite automata. International Journal of Computer Mathematics\u00a035, 117\u2013132 (1990)","journal-title":"International Journal of Computer Mathematics"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1080\/00207169408804276","volume":"51","author":"A. Fellah","year":"1994","unstructured":"Fellah, A.: Equations and regular-like expressions for AFA. International Journal of Computer Mathematics\u00a051, 157\u2013172 (1994)","journal-title":"International Journal of Computer Mathematics"},{"issue":"1","key":"5_CR18","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"Journal of the ACM"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","volume":"10","author":"J.A. Brzozowski","year":"1980","unstructured":"Brzozowski, J.A., Leiss, E.: On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science\u00a010, 19\u201335 (1980)","journal-title":"Theoretical Computer Science"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/S0304-3975(81)80005-9","volume":"13","author":"E. Leiss","year":"1981","unstructured":"Leiss, E.: Succinct representation of regular languages by Boolean automata. Theoretical Computer Science\u00a013, 323\u2013330 (1981)","journal-title":"Theoretical Computer Science"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/0304-3975(85)90215-4","volume":"38","author":"E. Leiss","year":"1985","unstructured":"Leiss, E.: Succinct representation of regular languages by Boolean automata II. Theoretical Computer Science\u00a038, 133\u2013136 (1985)","journal-title":"Theoretical Computer Science"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-48057-9_6","volume-title":"Automata Implementation","author":"S. Huerter","year":"1999","unstructured":"Huerter, S., et al.: Implementing reversed alternating finite automaton (r-AFA) operations. In: Champarnaud, J.-M., Maurel, D., Ziadi, D. (eds.) WIA 1998. LNCS, vol.\u00a01660, pp. 69\u201381. Springer, Heidelberg (1999)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0031391","volume-title":"Automata Implementation","author":"K. Salomaa","year":"1998","unstructured":"Salomaa, K., Wu, X., Yu, S.: Efficient implementation of regular languages using r-AFA. In: Wood, D., Yu, S. (eds.) WIA 1997. LNCS, vol.\u00a01436, pp. 176\u2013184. Springer, Heidelberg (1998)"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(99)00020-1","volume":"231","author":"K. Salomaa","year":"2000","unstructured":"Salomaa, K., Wu, X., Yu, S.: Efficient implementation of regular languages using reversed alternating finite automata. Theoretical Computer Science\u00a0231(1), 103\u2013111 (2000)","journal-title":"Theoretical Computer Science"},{"key":"5_CR25","unstructured":"Tuerk, T., Schneider, K.: Relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Internal Report 340, Department of Computer Science, University of Kaiserslautern (2005), http:\/\/kluedo.ub.uni-kl.de"},{"key":"5_CR26","unstructured":"B\u00e8s, A.: A survey of arithmetical definability. Bulletin of the Soci\u00e9t\u00e9 Math\u00e9matique Belgique, 1\u201354 (2002)"},{"key":"5_CR27","first-page":"191","volume":"1","author":"V. Bruyere","year":"1994","unstructured":"Bruyere, V., et al.: Logic and p-recognizable sets of integers. Bulletin of the Soci\u00e9t\u00e9 Math\u00e9matique Belgique\u00a01, 191\u2013238 (1994)","journal-title":"Bulletin of the Soci\u00e9t\u00e9 Math\u00e9matique Belgique"},{"issue":"1","key":"5_CR28","doi-asserted-by":"publisher","first-page":"155","DOI":"10.2307\/2042554","volume":"72","author":"J. Gathen von zur","year":"1978","unstructured":"von zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proceedings of the American Mathematical Society\u00a072(1), 155\u2013158 (1978)","journal-title":"Proceedings of the American Mathematical Society"},{"key":"5_CR29","volume-title":"An introduction to the theory of numbers","author":"G.H. Hardy","year":"1979","unstructured":"Hardy, G.H., Wright, E.M.: An introduction to the theory of numbers. Oxford University Press, Oxford (1979)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"5_CR31","unstructured":"Ranise, S., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2006), http:\/\/goedel.cs.uiowa.edu\/smtlib"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software, Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70889-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:11:13Z","timestamp":1605762673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70889-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540708889","9783540708896"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70889-6_5","relation":{},"subject":[]}}