{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T10:39:54Z","timestamp":1776940794012,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705888","type":"print"},{"value":"9783540705901","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_4","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"48-62","source":"Crossref","is-referenced-by-count":12,"title":["Finer Is Better: Abstraction Refinement for Rewriting Approximations"],"prefix":"10.1007","author":[{"given":"Yohan","family":"Boichut","sequence":"first","affiliation":[]},{"given":"Rom\u00e9o","family":"Courbis","sequence":"additional","affiliation":[]},{"given":"Pierre-Cyrille","family":"H\u00e9am","sequence":"additional","affiliation":[]},{"given":"Olga","family":"Kouchnarenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-73449-9_6","volume-title":"Term Rewriting and Applications","author":"Y. Boichut","year":"2007","unstructured":"Boichut, Y., Genet, T., Jensen, T., Le Roux, L.: Rewriting approximations for fast prototyping of static analyzers. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 48\u201362. Springer, Heidelberg (2007)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Boichut, Y., H\u00e9am, P.-C.: A Theoretical Limit for Safety Verification Techniques with Regular Fix-point Computations. Information Processing Letters ( to appear, 2008)","DOI":"10.1016\/j.ipl.2008.03.012"},{"key":"4_CR4","unstructured":"Boichut, Y., H\u00e9am, P.-C., Kouchnarenko, O.: Automatic Verification of Security Protocols Using Approximations. Technical Report RR-5727, INRIA (2005)"},{"key":"4_CR5","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking. In: proceedings of INFINITY. BRICS Notes Series, vol.\u00a04, pp. 15\u201324 (2005)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.: Counterexample-guided abstraction refinement. In: proceedings of TIME (2003)","DOI":"10.1109\/TIME.2003.1214874"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Lu, Y., Jha, S., Veith, H.: Tree-like counterexamples in model checking. In: proceedings of LICS, pp. 19\u201329 (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"key":"4_CR9","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications (2002)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36385-8","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Das","year":"2002","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: Handbook of Theoretical Computer Science, vol.\u00a0B, ch.6, pp. 244\u2013320. Elsevier Science Publishers B. V (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Feuillade, G., Genet, T., VietTriemTong, V.: Reachability analysis over term rewriting systems. Journal of Automated Reasonning\u00a033(3-4) (2004)","DOI":"10.1007\/s10817-004-6246-0"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/10721959_21","volume-title":"Automated Deduction - CADE-17","author":"T. Genet","year":"2000","unstructured":"Genet, T., Klay, F.: Rewriting for Cryptographic Protocol Verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 271\u2013290. Springer, Heidelberg (2000)"},{"key":"4_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1007\/3-540-45653-8_48","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Genet","year":"2001","unstructured":"Genet, T., Tong, V.V.T.: Reachability Analysis of Term Rewriting Systems with timbuk. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 691\u2013702. Springer, Heidelberg (2001)"},{"issue":"1\/2","key":"4_CR15","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/FI-1995-24127","volume":"24","author":"R. Gilleron","year":"1995","unstructured":"Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundamenta Informatica\u00a024(1\/2), 157\u2013174 (1995)","journal-title":"Fundamenta Informatica"},{"issue":"1-2","key":"4_CR16","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0304-3975(96)00333-7","volume":"194","author":"P. Gyenizse","year":"1998","unstructured":"Gyenizse, P., V\u00e1gv\u00f6lgyi, S.: Linear Generalized Semi-Monadic Rewrite Systems Effectively Preserve Recognizability. Theoretical Computer Science\u00a0194(1-2), 87\u2013122 (1998)","journal-title":"Theoretical Computer Science"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/3-540-61464-8_65","volume-title":"Rewriting Techniques and Applications","author":"F. Jacquemard","year":"1996","unstructured":"Jacquemard, F.: Decidable approximations of term rewriting systems. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 362\u2013376. Springer, Heidelberg (1996)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y. Lakhnech","year":"2001","unstructured":"Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental Verification by Abstraction. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031. Springer, Heidelberg (2001)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48294-6_10","volume-title":"Static Analysis","author":"D. Monniaux","year":"1999","unstructured":"Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694. Springer, Heidelberg (1999)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10721975_17","volume-title":"Rewriting Techniques and Applications","author":"T. Takai","year":"2000","unstructured":"Takai, T., Kaji, Y., Seki, H.: Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:23:55Z","timestamp":1620001435000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}