{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:49:29Z","timestamp":1725572969215},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540374060"},{"type":"electronic","value":"9783540374114"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11817963_10","type":"book-chapter","created":{"date-parts":[[2006,8,5]],"date-time":"2006-08-05T05:07:51Z","timestamp":1154754471000},"page":"67-80","source":"Crossref","is-referenced-by-count":11,"title":["Don\u2019t Care Words with an Application to the Automata-Based Approach for Real Addition"],"prefix":"10.1007","author":[{"given":"Jochen","family":"Eisinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast acceleration of symbolic transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-27813-9_25","volume-title":"Computer Aided Verification","author":"C. Bartzis","year":"2004","unstructured":"Bartzis, C., Bultan, T.: Widening arithmetic automata. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 321\u2013333. Springer, Heidelberg (2004)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-63166-6_18","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1997","unstructured":"Boigelot, B., Bronne, L., Rassart, S.: An improved reachability analysis method for strongly linear hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 167\u2013178. Springer, Heidelberg (1997)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-45069-6_19","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 193\u2013205. Springer, Heidelberg (2003)"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B. Boigelot","year":"2005","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM ToCL\u00a06, 614\u2013633 (2005)","journal-title":"ACM ToCL"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.tcs.2003.10.002","volume":"313","author":"B. Boigelot","year":"2004","unstructured":"Boigelot, B., Latour, L.: Counting the solutions of Presburger equations without enumerating them. TCS\u00a0313, 17\u201329 (2004)","journal-title":"TCS"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-540-24730-2_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Boigelot","year":"2004","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 561\u2013575. Springer, Heidelberg (2004)"},{"key":"10_CR8","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. Zeitschrift der mathematischen Logik und Grundlagen der Mathematik\u00a06, 66\u201392 (1960)","journal-title":"Zeitschrift der mathematischen Logik und Grundlagen der Mathematik"},{"key":"10_CR9","unstructured":"On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science. Stanford University Press, pp. 1\u201311 (1962)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Eisinger, J., Klaedtke, F.: Don\u2019t care words with an application to the automata-based approach for real addition, Tech. Rep. 223, Institut f\u00fcr Informatik, Albert-Ludwigs-Universit\u00e4t Freiburg (2006)","DOI":"10.1007\/11817963_10"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: LICS 1996, pp. 278\u2013292 (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1145\/266021.266068","volume-title":"DAC 1997","author":"Y. Hong","year":"1997","unstructured":"Hong, Y., Beerel, P.A., Burch, J.R., McMillan, K.L.: Safe BDD minimization using don\u2019t cares. In: DAC 1997, pp. 208\u2013213. ACM Press, New York (1997)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E.: An n logn algorithm for minimizing the states in a finite automaton. In: Theory of Machines and Computations, pp. 189\u2013196 (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM ToCL\u00a02, 408\u2013429 (2001)","journal-title":"ACM ToCL"},{"key":"10_CR15","unstructured":"LASH, The Li\u00e8ge Automata-based Symbolic Handler, http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"10_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0020-0190(00)00183-6","volume":"79","author":"C. L\u00f6ding","year":"2001","unstructured":"L\u00f6ding, C.: Efficient minimization of deterministic weak \u03c9-automata. IPL\u00a079, 105\u2013109 (2001)","journal-title":"IPL"},{"key":"10_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"10_CR18","first-page":"379","volume":"10","author":"L. Staiger","year":"1974","unstructured":"Staiger, L., Wagner, K.: Automatentheoretische und automatenfreie Charakterisierungen topologischer Klassen regul\u00e4rer Folgenmengen. Elektronische Informationsverarbeitung und Kybernetik\u00a010, 379\u2013392 (1974)","journal-title":"Elektronische Informationsverarbeitung und Kybernetik"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11513988_40","volume-title":"Computer Aided Verification","author":"T. Yavuz-Kahveci","year":"2005","unstructured":"Yavuz-Kahveci, T., Bartzis, C., Bultan, T.: Action language verifier, extended. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 413\u2013417. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11817963_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:15:54Z","timestamp":1605644154000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11817963_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540374060","9783540374114"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11817963_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}