{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T21:11:49Z","timestamp":1791061909108,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_46","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"539-554","source":"Crossref","is-referenced-by-count":30,"title":["Extrapolating Tree Transformations"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"46_CR1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Robert K. Brayton, Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Partial-order reduction in symbolic state space exploration. In Computer Aided Verification, pages 340\u2013351, 1997.","DOI":"10.1007\/3-540-63166-6_34"},{"key":"46_CR2","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"P. Abdulla","year":"1998","unstructured":"P. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In CAV\u201998. LNCS 1427, 1998."},{"key":"46_CR3","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. Lecture Notes in Com-puter Science, 1633:134\u2013150, 1999.","DOI":"10.1007\/3-540-48683-6_14"},{"key":"46_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u2019 97","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability Analysis of Pushdown Automata: Application to Model Checking. In CONCUR\u2019 97. LNCS 1243, 1997."},{"key":"46_CR5","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In CAV\u201900. LNCS, 2000."},{"key":"46_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, A. Muscholl, and T. Touili. Permutation Rewriting and Algorithmic Verification. In LICS\u201901. IEEE, 2001.","DOI":"10.1109\/LICS.2001.932515"},{"key":"46_CR7","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201901","author":"A. Bouajjani","year":"2001","unstructured":"A. Bouajjani. Languages, Rewriting systems, and Verification of Infinte-State Systems. In ICALP\u201901. LNCS 2076, 2001. invited paper."},{"key":"46_CR8","doi-asserted-by":"crossref","unstructured":"A. Bouajjani and T. Touili. Extrapolating tree transformations. Technical report, LIAFA, May 2002. http:\/\/verif.liafa.jussieu.fr\/~touili .","DOI":"10.1007\/3-540-45657-0_46"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Recursive Procedures. In IFIP Conf. on Formal Description of Programming Concepts. North-Holland Pub., 1977.","DOI":"10.1145\/390017.808314"},{"key":"46_CR10","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u20192001","author":"H. Comon","year":"2001","unstructured":"H. Comon, V. Cortier, and J. Mitchell. Tree automata with one memory, set constraints and ping-pong protocols. In ICALP\u20192001. LNCS 2076, 2001."},{"key":"46_CR11","unstructured":"H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http:\/\/www.grappa.univ-lille3.fr\/tata , 1997."},{"key":"46_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BFb0016951","volume-title":"Verifying parameterised networks using abstraction and regular languages","author":"E. M. Clarke","year":"1995","unstructured":"E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterised networks using abstraction and regular languages. Lecture Notes in Computer Science, 962:395\u2013407, 1995."},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL\u201978. ACM, 1978.","DOI":"10.1145\/512760.512770"},{"key":"46_CR14","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"D. Dams","year":"2001","unstructured":"Dennis Dams, Yassine Lakhnech, and Martin Steffen\u201d. Iterating transducers. In CAV\u201901. LNCS, 2001."},{"key":"46_CR15","series-title":"Lect Notes Comput Sci","volume-title":"FOSSACS\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In FOSSACS\u201999, volume LNCS 1578, 1999."},{"key":"46_CR16","doi-asserted-by":"crossref","unstructured":"Joost Engelfriet. Bottom-up and top-down tree transformations-a comparison. In Mathematical Systems Theory, volume 9(3), 1975.","DOI":"10.1007\/BF01704020"},{"key":"46_CR17","doi-asserted-by":"crossref","unstructured":"Javier Esparza and Andreas Podelski. Efficient algorithms for pre * and post * on interprocedural parallel flow graphs. In Symposium on Principles of Programming Languages, pages 1\u201311, 2000.","DOI":"10.1145\/325694.325697"},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"L. Fribourg and H. Olsen. Reachability sets of parametrized rings as regular languages. In Infinity\u201997. volume 9 of Electronical Notes in Theoretical Computer Science. Elsevier Science, 1997.","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"46_CR19","series-title":"Lect Notes Comput Sci","volume-title":"15th IPDPS 2000 Workshops","author":"J. Goubault-Larrecq","year":"2000","unstructured":"J. Goubault-Larrecq. A method for automatic cryptographic protocol verification. In 15th IPDPS 2000 Workshops. LNCS 1800, 2000."},{"key":"46_CR20","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/FI-1995-24127","volume":"24","author":"R. Gilleron","year":"1995","unstructured":"R. Gilleron and S. Tison. Regular tree languages and rewrite systems. In Fundamenta Informaticae, volume 24, pages 157\u2013175, 1995.","journal-title":"Fundamenta Informaticae"},{"key":"46_CR21","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201900","author":"B. Jonsson","year":"2000","unstructured":"B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS\u201900. LNCS, 2000."},{"key":"46_CR22","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Proc. CAV\u201997","author":"K.M.M.+.9.7._.Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In O. Grumberg, editor, Proc. CAV\u201997, volume 1254 of LNCS, pages 424\u2013435. Springer, 1997."},{"key":"46_CR23","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/BFb0055615","volume":"1466","author":"D. Lugiez","year":"1998","unstructured":"D. Lugiez and Ph. Schnoebelen. The regular viewpoint on PA-processes. In Proc. 9th Int. Conf. Concurrency Theory (CONCUR\u201998), Nice, France, Sep. 1998, volume 1466, pages 50\u201366. Springer, 1998.","journal-title":"Proc. 9th Int. Conf. Concurrency Theory (CONCUR\u201998), Nice, France, Sep. 1998"},{"key":"46_CR24","unstructured":"R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, TUM, 1998."},{"key":"46_CR25","doi-asserted-by":"crossref","unstructured":"D. Monniaux. Abstracting cryptographic protocols with tree automata. Science of Computer Programming, 2002.","DOI":"10.1016\/S0167-6423(02)00132-6"},{"key":"46_CR26","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Liveness and acceleration in parametrized verification. In CAV\u201900. LNCS, 2000."},{"key":"46_CR27","doi-asserted-by":"crossref","unstructured":"T. Touili. Widening Techniques for Regular Model Checking. In Vepas Workshop. Volume 50 of Electronic Notes in TCS, 2001.","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"46_CR28","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"P. Wolper","year":"1998","unstructured":"Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular stae spaces. In CAV\u201998. LNCS 1254, 1998."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:34:53Z","timestamp":1683844493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_46","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}