{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:03:59Z","timestamp":1725566639901},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_35","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"484-499","source":"Crossref","is-referenced-by-count":18,"title":["On Computing Reachability Sets of Process Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"Ammirati, P., Delzanno, G., Ganty, P., Geeraerts, G., Raskin, J.-F., Van Begin, L.: Babylon: An integrated toolkit for the specification and verification of parameterized systems. In: SAVE 2002 (2002)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_32","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2000","unstructured":"Annichini, A., Asarin, E., Bouajjani, A.: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A Tool for Reachability Analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 368. Springer, Heidelberg (2001)"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-45319-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 158. Springer, Heidelberg (2001)"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45319-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2001","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking c programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 268. Springer, Heidelberg (2001)"},{"key":"35_CR6","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":"35_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 223\u2013235. Springer, Heidelberg (2003)"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1994","unstructured":"Boigelot, B., Wolper, P.: Symbolic Verification with Periodic Sets. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, Springer, Heidelberg (1994)"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (1997)"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: Proc. of the 30th ACM Symp. on Principles of Programming Languages, POPL 2003 (2003)","DOI":"10.1145\/604131.604137"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: Reachability Analysis of Synchronized PA Systems. In: Proc. Infinity Workshop (2004)","DOI":"10.1016\/j.entcs.2005.02.063"},{"key":"35_CR12","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":"35_CR13","unstructured":"Bruggemann-Klein, A., Murata, M., Wood, D.: Regular tree and regular hedge languages over unranked alphabets. Research report (2001)"},{"key":"35_CR14","volume-title":"Proc. of the Intern. Symp. on Software Testing and Analysis","author":"T. Bultan","year":"1998","unstructured":"Bultan, T., Gerber, R., League, C.: Verifying Systems With Integer Constraints and Boolean Predicates: A Composite Approach. In: Proc. of the Intern. Symp. on Software Testing and Analysis, ACM press, New York (1998)"},{"key":"35_CR15","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. Theoret. Comput. Sci.\u00a0106, 61\u201386 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"35_CR16","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proc. Infinity Workshop","author":"T. Colcombet","year":"2002","unstructured":"Colcombet, T.: Rewriting in the partial algebra of typed terms modulo ac. In: Proc. Infinity Workshop. Electronic Notes in Theoretical Computer Science, vol.\u00a068, Elsevier Science Pub., Amsterdam (2002)"},{"key":"35_CR17","volume-title":"POPL 1978","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, ACM, New York (1978)"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-44585-4_28","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Van Begin, L., Raskin, J.-F.: Attacking symbolic state explosion in parametrized verification. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 298. Springer, Heidelberg (2001)"},{"key":"35_CR19","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., Van Begin, L., Raskin, J.-F.: Toward the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 173. Springer, Heidelberg (2002)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Fundamentals of Computation Theory","author":"J. Esparza","year":"1995","unstructured":"Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. In: Reichel, H. (ed.) FCT 1995. LNCS, vol.\u00a0965, Springer, Heidelberg (1995)"},{"key":"35_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-45711-9_16","volume-title":"Formal and Natural Computing","author":"J. Esparza","year":"2002","unstructured":"Esparza, J.: Grammars as processes. In: Brauer, W., Ehrig, H., Karhum\u00e4ki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol.\u00a02300, p. 277. Springer, Heidelberg (2002)"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"SPIN Model Checking and Software Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithm for model checking pushdown systems. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, Springer, Heidelberg (2000)"},{"key":"35_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Esparza, J., Melzer, S.: Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design\u00a016 (2000)","DOI":"10.1023\/A:1008743212620"},{"key":"35_CR25","first-page":"85","volume":"52","author":"J. Esparza","year":"1994","unstructured":"Esparza, J., Nielsenl, M.: Decidability issues for Petri nets - a survey. Bulletin of the EATCS\u00a052, 85\u2013107 (1994)","journal-title":"Bulletin of the EATCS"},{"key":"35_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"35_CR27","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre * and post * on interprocedural parallel flow graphs. In: Symposium on Principles of Programming Languages, pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"key":"35_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A Direct Symbolic Approach to Model Checking Pushdown Systems. In: Infinity 1997 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"35_CR30","doi-asserted-by":"crossref","unstructured":"Hopcroft, J., Pansiot, J.-J.: On The Reachability Problem for 5-Dimensional Vector Addition Systems. Theoret. Comput. Sci.\u00a08 (1979)","DOI":"10.1016\/0304-3975(79)90041-0"},{"key":"35_CR31","unstructured":"The Li\u00e8ge Automata-based Symbolic Handler, LASH (2001), Available at http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"35_CR32","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":"35_CR33","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":"35_CR34","unstructured":"Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, Techn. Univ. of Munich (1998)"},{"key":"35_CR35","volume-title":"POPL 2004","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Rajamani, S.K., Rehof, J.: Procedure Summaries for Model Checking Multithreaded Software. In: POPL 2004, ACM, New York (2004)"},{"key":"35_CR36","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit \u00e4t M\u00fcnchen (2002)"},{"key":"35_CR37","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":"35_CR38","unstructured":"Touili, T.: Analyse symbolique de syst\u00e8mes infinis bas\u00e9e sur les automates: Application \u00e0 la v\u00e9rification de syst\u00e8mes param\u00e9tr\u00e9s et dynamiques. Phd. thesis, University of Paris 7 (2003)"},{"key":"35_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying Systems with Infinite but Regular State Spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T19:02:39Z","timestamp":1636570959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}