{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:19Z","timestamp":1760202559809},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,1,25]],"date-time":"2008-01-25T00:00:00Z","timestamp":1201219200000},"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":[[2008,4]]},"DOI":"10.1007\/s10703-008-0048-7","type":"journal-article","created":{"date-parts":[[2008,1,24]],"date-time":"2008-01-24T20:12:50Z","timestamp":1201205570000},"page":"129-172","source":"Crossref","is-referenced-by-count":22,"title":["Verification of parametric concurrent systems with\u00a0prioritised FIFO resource management"],"prefix":"10.1007","volume":"32","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Habermehl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2008,1,25]]},"reference":[{"key":"48_CR1","series-title":"LNCS","volume-title":"Proc. of CAV\u201999","author":"P Abdulla","year":"1999","unstructured":"Abdulla P, Bouajjani A, Jonsson B, Nilsson M (1999) Handling global conditions in parametrized system verification. In: Proc. of CAV\u201999. LNCS, vol 1633. Springer, New York"},{"issue":"6","key":"48_CR2","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K Apt","year":"1986","unstructured":"Apt K, Kozen D (1986) Limits for automatic verification of finite-state concurrent systems. Inf Process Lett 22(6):307\u2013309","journal-title":"Inf Process Lett"},{"key":"48_CR3","series-title":"LNCS","volume-title":"Proc. of FME\u201902","author":"T Arts","year":"2002","unstructured":"Arts T, Earle CB, Derrick J (2002) Verifying Erlang code: a resource locker case-study. In: Proc. of FME\u201902. LNCS, vol 2391. Springer, New York"},{"key":"48_CR4","series-title":"LNCS","volume-title":"Proc. of TACAS 2000","author":"K Baukus","year":"2000","unstructured":"Baukus K, Bensalem S, Lakhnech Y, Stahl K (2000) Abstracting WS1S systems to verify prameterized networks. In: Proc. of TACAS 2000. LNCS, vol 1785. Springer, New York"},{"key":"48_CR5","series-title":"LNCS","volume-title":"Proc. of CADE 2000","author":"EA Emerson","year":"2000","unstructured":"Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: Proc. of CADE 2000. LNCS, vol 1831. Springer, New York"},{"key":"48_CR6","series-title":"LNCS","volume-title":"Proc. of TACAS\u201902","author":"EA Emerson","year":"2002","unstructured":"Emerson EA, Kahlon V (2002) Model checking large-scale and parameterized resource allocation systems. In: Proc. of TACAS\u201902. LNCS, vol 2280. Springer, New York"},{"key":"48_CR7","volume-title":"Proc. of POPL\u201995","author":"EA Emerson","year":"1995","unstructured":"Emerson EA, Namjoshi KS (1995) Reasoning about rings. In: Proc. of POPL\u201995. ACM, New York"},{"key":"48_CR8","series-title":"LNCS","volume-title":"Proc. of CAV\u201996","author":"EA Emerson","year":"1996","unstructured":"Emerson EA, Namjoshi KS (1996) Automatic verification of parameterized synchronous systems. In: Proc. of CAV\u201996. LNCS, vol 1102. Springer, New York"},{"issue":"4","key":"48_CR9","doi-asserted-by":"crossref","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"EA Emerson","year":"1997","unstructured":"Emerson EA, Sistla AP (1997) Utilizing symmetry when model checking under fairness assumptions: an automata-theoretic approach. ACM Trans Program Lang Syst 19(4):617\u2013638","journal-title":"ACM Trans Program Lang Syst"},{"issue":"3","key":"48_CR10","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 ACM 39(3):675\u2013735","journal-title":"J ACM"},{"key":"48_CR11","series-title":"LNCS","volume-title":"Proc. of CAV\u201997","author":"Y Kesten","year":"1997","unstructured":"Kesten Y, Maler O, Marcus M, Pnueli A, Shahar E (1997) Symbolic model checking with rich assertional languages. In: Proc. of CAV\u201997. LNCS, vol 1254. Springer, New York"},{"key":"48_CR12","doi-asserted-by":"crossref","unstructured":"Kurshan RP, McMillan KL (1995) A structural induction theorem for processes. Inf. Comput., 117(1)","DOI":"10.1006\/inco.1995.1024"},{"key":"48_CR13","series-title":"LNCS","volume-title":"Proc. of TACAS\u201901","author":"A Pnueli","year":"2001","unstructured":"Pnueli A, Ruah S, Zuck L (2001) Automatic deductive verification with invisible invariants. In: Proc. of TACAS\u201901. LNCS, vol 2031. Springer, New York"},{"key":"48_CR14","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1090\/S0002-9939-1978-0500555-0","volume":"72","author":"J Zur Gathen von","year":"1978","unstructured":"von Zur Gathen J, Sieveking M (1978) A bound on solutions of linear integer equalities and inequalities. Proc Am Math Soc 72:155\u2013158","journal-title":"Proc Am Math Soc"},{"key":"48_CR15","series-title":"LNCS","volume-title":"Proc of int workshop on automatic verification methods for finite state systems","author":"P Wolper","year":"1989","unstructured":"Wolper P, Lovinfosse V (1989) Verifying properties of large sets of processes with network invariants. In: Proc of int workshop on automatic verification methods for finite state systems. LNCS, vol 407. Springer, New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0048-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0048-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0048-7","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-0048-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,1,25]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,4]]}},"alternative-id":["48"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0048-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,1,25]]}}}