{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:56:59Z","timestamp":1725490619806},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_17","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"145-157","source":"Crossref","is-referenced-by-count":39,"title":["Parameterized Verification of Infinite-State Processes with Global Conditions"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Giorgio","family":"Delzanno","sequence":"additional","affiliation":[]},{"given":"Ahmed","family":"Rezine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation\u00a0160, 109\u2013127 (2000)","journal-title":"Information and Computation"},{"key":"17_CR2","unstructured":"Abdulla, P.A., Delzanno, G.: On the coverability problem for constrained multiset rewriting. In: Proc. AVIS 2006"},{"key":"17_CR3","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized Verification of Infinite-state Processes with Global Conditions, Technical Report 2007-014, Uppsala University (April 2007)"},{"key":"17_CR4","unstructured":"Abdulla, P.A., Henda, N.B., Delzanno, G., Rezine, A.: Regular model checking without transducers. In: Proc. TACAS 2007 (to appear, 2007)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2002 - Concurrency Theory","author":"P.A. Abdulla","year":"2002","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, Springer, Heidelberg (2002)"},{"key":"17_CR6","volume-title":"Foundations of Multithreaded, Parallel, and Distributed Programming","author":"G. Andrews","year":"2000","unstructured":"Andrews, G.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison-Wesley, Reading (2000)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Concurrent Object-Oriented Programming and Petri Nets","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: Agha, G.A., De Cindio, F., Rozenberg, G. (eds.) Concurrent Object-Oriented Programming and Petri Nets. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2003)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Beyond parameterized verification. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, Springer, Heidelberg (2002)"},{"issue":"4","key":"17_CR10","doi-asserted-by":"publisher","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T. Bultan","year":"1999","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Model-checking concurrent systems with unbounded integer variables. ACM TOPLAS\u00a021(4), 747\u2013789 (1999)","journal-title":"ACM TOPLAS"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 126\u2013141. Springer, Heidelberg (2005)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_8","volume-title":"Computer Aided Verification","author":"G. Delzanno","year":"2000","unstructured":"Delzanno, G.: Automatic verification of cache coherence protocols. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: On model checking for non-deterministic infinite-state systems. In: Proc. LICS 1998 (1998)","DOI":"10.1109\/LICS.1998.705644"},{"key":"17_CR14","volume-title":"Proc. LICS\u2019 99, 14 th IEEE Int. Symp.","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proc. LICS\u2019 99, 14\n                    th\n                   IEEE Int. Symp., IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Logic Program Synthesis and Transformation","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Richardson, J.: Symbolic verification with gap-order constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, Springer, Heidelberg (1997)"},{"issue":"3","key":"17_CR16","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many identical processes. Journal of the ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"Journal of the ACM"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. TCS\u00a0256, 93\u2013112 (2001)","journal-title":"TCS"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 135\u2013147. Springer, Heidelberg (2004)"},{"issue":"8","key":"17_CR19","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"1","key":"17_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P. Revesz","year":"1993","unstructured":"Revesz, P.: A closed form evaluation for datalog queries with integer (gap)-order constraints. Theoretical Computer Science\u00a0116(1), 117\u2013149 (1993)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G. Ricart","year":"1981","unstructured":"Ricart, G., Agrawal, A.K.: An optimal algorithm for mutual exclusion in computer networks. Communications of the ACM\u00a024(1), 9\u201317 (1981)","journal-title":"Communications of the ACM"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Sedletsky, E., Pnueli, A., Ben-Ari, M.: Formal verification of the ricart-agrawala algorithm. In: Proc. FSTTCS 2000 (2000)","DOI":"10.1007\/3-540-44450-5_26"},{"key":"17_CR23","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. LICS 1986 (June 1986)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:24Z","timestamp":1619518104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_17","relation":{},"subject":[]}}