{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:17:54Z","timestamp":1760015874094},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,12,17]],"date-time":"2008-12-17T00:00:00Z","timestamp":1229472000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10703-008-0062-9","type":"journal-article","created":{"date-parts":[[2008,12,16]],"date-time":"2008-12-16T17:51:26Z","timestamp":1229449886000},"page":"126-156","source":"Crossref","is-referenced-by-count":15,"title":["Approximated parameterized verification of infinite-state processes with global conditions"],"prefix":"10.1007","volume":"34","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","published-online":{"date-parts":[[2008,12,17]]},"reference":[{"key":"62_CR1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"PA Abdulla","year":"2000","unstructured":"Abdulla PA, \u010cer\u0101ns K, Jonsson B, Tsay YK (2000) Algorithmic analysis of programs with well quasi-ordered domains. Inf Comput 160:109\u2013127","journal-title":"Inf Comput"},{"key":"62_CR2","unstructured":"Abdulla PA, Delzanno G (2006) On the coverability problem for constrained multiset rewriting. In: Proc AVIS\u201906, 5th int workshop automated verification of infinite-state systems"},{"key":"62_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Proc 19th int conf on computer aided verification","author":"PA Abdulla","year":"2007","unstructured":"Abdulla PA, Delzanno G, Rezine A (2007) Parameterized verification of infinite-state processes with global conditions. In: Proc 19th int conf on computer aided verification. Lecture notes in computer science, vol 4590. Springer, Berlin, pp 145\u2013157"},{"key":"62_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-540-85762-4_4","volume-title":"ICTAC","author":"PA Abdulla","year":"2008","unstructured":"Abdulla PA, Delzanno G, Rezine A (2008) Monotonic abstraction in action (automatic verification of distributed mutex algorithms). In: Yenig\u00fcn H (ed) ICTAC. Lecture notes in computer science, vol\u00a05160. Springer, Berlin, pp\u00a050\u201365"},{"key":"62_CR5","unstructured":"Abdulla PA, Henda NB, Delzanno G, Rezine A (2007) Regular model checking without transducers (on efficient verification of parameterized systems). In: Proc TACAS \u201907, 13th int conf on tools and algorithms for the construction and analysis of systems"},{"key":"62_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1007\/3-540-45694-5_9","volume-title":"Proc CONCUR 2002, 13th int conf on concurrency theory","author":"PA Abdulla","year":"2002","unstructured":"Abdulla PA, Jonsson B, Nilsson M, d\u2019Orso J (2002) Regular model checking made simple and efficient. In: Proc CONCUR 2002, 13th int conf on concurrency theory. Lecture notes in computer science, vol\u00a02421. Springer, Berlin, pp 116\u2013130"},{"key":"62_CR7","volume-title":"Foundations of multithreaded, parallel, and distributed programming","author":"G Andrews","year":"2000","unstructured":"Andrews G (2000) Foundations of multithreaded, parallel, and distributed programming. Addison Wesley, Reading"},{"key":"62_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Proc 13th int conf on computer aided verification","author":"T Arons","year":"2001","unstructured":"Arons T, Pnueli A, Ruah S, Xu J, Zuck L (2001) Parameterized verification with automatically computed inductive assertions. In: Berry G, Comon H, Finkel A (eds) Proc 13th int conf on computer aided verification. Lecture notes in computer science, vol\u00a02102. Springer, Berlin, pp\u00a0221\u2013234"},{"key":"62_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-45069-6_24","volume-title":"Proc 15th int conf on computer aided verification","author":"B Boigelot","year":"2003","unstructured":"Boigelot B, Legay A, Wolper P (2003) Iterating transducers in the large. In: Proc 15th int conf on computer aided verification. Lecture notes in computer science, vol 2725. Springer, Berlin, pp 223\u2013235"},{"key":"62_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani A, Habermehl P, Rogalewicz A, Vojnar T (2006) Abstract tree regular model checking of complex dynamic data structures. In: Proc 13th int symp on static analysis","DOI":"10.1007\/11823230_5"},{"key":"62_CR11","first-page":"221","volume-title":"Proc TACAS \u201902, 8th int conf on tools and algorithms for the construction and analysis of systems","author":"M Bozzano","year":"2002","unstructured":"Bozzano M, Delzanno G (2002) Beyond parameterized verification. In: Proc TACAS \u201902, 8th int conf on tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol\u00a02280. Springer, Berlin, pp 221\u2013235"},{"issue":"4","key":"62_CR12","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T Bultan","year":"1999","unstructured":"Bultan T, Gerber R, Pugh W (1999) Model-checking concurrent systems with unbounded integer variables. ACM Trans Program Lang Syst 21(4):747\u2013789","journal-title":"ACM Trans Program Lang Syst"},{"key":"62_CR13","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/11734666","volume-title":"Proc VMCAI \u201906, 7th int conf on verification, model checking, and abstract interpretation","author":"E Clarke","year":"2006","unstructured":"Clarke E, Talupur M, Veith H (2006) Environment abstraction for parameterized verification. In: Proc VMCAI \u201906, 7th int conf on verification, model checking, and abstract interpretation. Lecture notes in computer science, vol\u00a03855. Springer, Berlin, pp\u00a0126\u2013141"},{"key":"62_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Proc. 12th int conf on computer aided verification","author":"G Delzanno","year":"2000","unstructured":"Delzanno G (2000) Automatic verification of cache coherence protocols. In: Emerson EA, Sistla AP (eds) Proc. 12th int conf on computer aided verification. Lecture notes in computer science, vol\u00a01855. Springer, Berlin, pp 53\u201368"},{"key":"62_CR15","doi-asserted-by":"crossref","unstructured":"Emerson E, Namjoshi K (1998) On model checking for non-deterministic infinite-state systems. In: Proc LICS \u201998, 13th IEEE int symp on logic in computer science, pp\u00a070\u201380","DOI":"10.1109\/LICS.1998.705644"},{"key":"62_CR16","doi-asserted-by":"crossref","unstructured":"Esparza J, Finkel A, Mayr R (1999) On the verification of broadcast protocols. In: Proc LICS \u201999, 14th IEEE int symp on logic in computer science","DOI":"10.1109\/LICS.1999.782630"},{"key":"62_CR17","series-title":"Lecture notes in computer science","volume-title":"LOPSTR\u201996","author":"L Fribourg","year":"1997","unstructured":"Fribourg L, Richardson J (1997) Symbolic verification with gap-order constraints. In: LOPSTR\u201996. Lecture notes in computer science, vol\u00a01207. Springer, Berlin"},{"issue":"3","key":"62_CR18","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German SM, Sistla AP (1992) Reasoning about systems with many processes. J\u00a0ACM 39(3):675\u2013735","journal-title":"J\u00a0ACM"},{"key":"62_CR19","doi-asserted-by":"crossref","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 (2001) Symbolic model checking with rich assertional languages. Theor Comput Sci 256:93\u2013112","journal-title":"Theor Comput Sci"},{"key":"62_CR20","doi-asserted-by":"crossref","unstructured":"Lahiri SK, Bryant RE (2004) Indexed predicate discovery for unbounded system verification. In: CAV 2004, pp\u00a0135\u2013147","DOI":"10.1007\/978-3-540-27813-9_11"},{"issue":"8","key":"62_CR21","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport L (1974) A new solution of Dijkstra\u2019s concurrent programming problem. Commun ACM 17(8):453\u2013455","journal-title":"Commun ACM"},{"issue":"1","key":"62_CR22","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P Revesz","year":"1993","unstructured":"Revesz P (1993) A closed form evaluation for datalog queries with integer (gap)-order constraints. Theor Comput Sci 116(1):117\u2013149","journal-title":"Theor Comput Sci"},{"key":"62_CR23","unstructured":"Rezine A (2008) Parameterized systems: Generalizing and simplifying automatic verification. PhD thesis, Uppsala University"},{"key":"62_CR24","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: Proc LICS \u201986, 1st IEEE int symp on logic in computer science, pp\u00a0332\u2013344"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0062-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0062-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0062-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0062-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,17]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["62"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0062-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,12,17]]}}}