{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:27Z","timestamp":1762458507875},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540368342"},{"type":"electronic","value":"9783540368359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11805618_11","type":"book-chapter","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:29:13Z","timestamp":1153837753000},"page":"136-150","source":"Crossref","is-referenced-by-count":11,"title":["Rewriting Models of Boolean Programs"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11590156_28","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 348\u2013359. Springer, Heidelberg (2005)"},{"issue":"4","key":"11_CR4","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1142\/S0129054103001893","volume":"14","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. Int. J. Found. Comput. Sci.\u00a014(4), 551\u2013582 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.entcs.2005.02.063","volume":"138","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: Reachability analysis of synchronized pa systems. Electr. Notes Theor. Comput. Sci.\u00a0138(3), 153\u2013178 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., M\u00fcller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-24597-1_7","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Touili, T.: Reachability analysis of process rewrite systems. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 74\u201387. Springer, Heidelberg (2003)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-540-32033-3_35","volume-title":"Term Rewriting and Applications","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Touili, T.: On computing reachability sets of process rewrite systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 484\u2013499. Springer, Heidelberg (2005)"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF01969548","volume":"6","author":"J.R. B\u00fcchi","year":"1964","unstructured":"B\u00fcchi, J.R.: Regular canonical systems. Arch. Math. Logik Grundlag.\u00a06, 91\u2013111 (1964)","journal-title":"Arch. Math. Logik Grundlag."},{"key":"11_CR10","volume-title":"The collected works of J. Richard B\u00fcchi","author":"J.R. B\u00fcchi","year":"1990","unstructured":"B\u00fcchi, J.R.: The collected works of J. Richard B\u00fcchi. Springer, New-York (1990)"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on Infinite Structures. In: Handbook of Process Algebra. North-Holland, Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/0304-3975(92)90278-N","volume":"106","author":"D. Caucal","year":"1992","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci.\u00a0106(1), 61\u201386 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: ACM Conference on Computer and Communications Security, pp. 235\u2013244 (2002)","DOI":"10.1145\/586110.586142"},{"issue":"5","key":"11_CR14","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"issue":"1","key":"11_CR17","doi-asserted-by":"crossref","first-page":"13","DOI":"10.3233\/FI-1997-3112","volume":"31","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Inform.\u00a031(1), 13\u201325 (1997)","journal-title":"Fundam. Inform."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL, pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"issue":"1\u20132","key":"11_CR20","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci.\u00a0256(1\u20132), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electr. Notes Theor. Comput. Sci.\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(79)90041-0","volume":"8","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Pansiot, J.-J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci.\u00a08, 135\u2013159 (1979)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"11_CR24","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0019-9958(83)80022-9","volume":"57","author":"D.T. Huynh","year":"1983","unstructured":"Huynh, D.T.: Commutative grammars: The complexity of uniform word problems. Information and Control\u00a057(1), 21\u201339 (1983)","journal-title":"Information and Control"},{"key":"11_CR25","first-page":"267","volume-title":"STOC","author":"S.R. Kosaraju","year":"1982","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC, pp. 267\u2013281. ACM, New York (1982)"},{"key":"11_CR26","unstructured":"Lipton, R.: The Reachability Problem Requires Exponential Space. Technical Report\u00a062, Yale University (1976)"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-36576-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"D. Lugiez","year":"2003","unstructured":"Lugiez, D.: Counting and Equality Constraints for Multitree Automata. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 328\u2013342. Springer, Heidelberg (2003)"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BFb0055615","volume-title":"CONCUR \u201998 Concurrency Theory","author":"D. Lugiez","year":"1998","unstructured":"Lugiez, D., Schnoebelen, P.: The Regular Viewpoint on PA-Processes. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 50\u201366. Springer, Heidelberg (1998)"},{"key":"11_CR29","first-page":"238","volume-title":"STOC","author":"E.W. Mayr","year":"1981","unstructured":"Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: STOC, pp. 238\u2013246. ACM, New York (1981)"},{"key":"11_CR30","unstructured":"Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (1998)"},{"issue":"1\u20132","key":"11_CR31","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1006\/inco.1999.2826","volume":"156","author":"R. Mayr","year":"2000","unstructured":"Mayr, R.: Process rewrite systems. Inf. Comput.\u00a0156(1\u20132), 264\u2013286 (2000)","journal-title":"Inf. Comput."},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"key":"11_CR33","volume-title":"PODS 2003","author":"H. Seidl","year":"2003","unstructured":"Seidl, H., Schwentick, T., Muscholl, A.: Numerical Document Queries. In: PODS 2003. ACM press, New York (2003)"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-540-31980-1_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Suwimonteerabuth","year":"2005","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java bytecode checker based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 541\u2013545. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11805618_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:12:44Z","timestamp":1605643964000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11805618_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540368342","9783540368359"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/11805618_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}