{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:13:10Z","timestamp":1781892790350,"version":"3.54.5"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T00:00:00Z","timestamp":1477267200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Madrid Regional Government","award":["project S2013\/ICE-2731, N-Greens Software-Next-GeneRation Energy-EfficieNt Secure Software"],"award-info":[{"award-number":["project S2013\/ICE-2731, N-Greens Software-Next-GeneRation Energy-EfficieNt Secure Software"]}]},{"name":"Spanish Ministry of Economy and Competitiveness","award":["project No. TIN2015-71819-P, RISCO-RIgorous analysis of Sophisticated COncurrent and distributed systems"],"award-info":[{"award-number":["project No. TIN2015-71819-P, RISCO-RIgorous analysis of Sophisticated COncurrent and distributed systems"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-016-0258-3","type":"journal-article","created":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T09:23:52Z","timestamp":1477301032000},"page":"140-167","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model checking parameterized asynchronous shared-memory systems"],"prefix":"10.1007","volume":"50","author":[{"given":"Antoine","family":"Durand-Gasselin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,10,24]]},"reference":[{"issue":"2","key":"258_CR1","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.ic.2005.05.008","volume":"202","author":"PA Abdulla","year":"2005","unstructured":"Abdulla PA, Bertrand N, Rabinovich A, Schnoebelen P (2005) Verification of probabilistic systems with faulty communication. Inf Comput 202(2):105\u2013228","journal-title":"Inf Comput"},{"key":"258_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla PA, Cerans K, Jonsson B, Tsay Y-K (1996) General decidability theorems for infinite-state systems. In: LICS \u201996, IEEE Computer Society, Washington, DC, pp 313\u2013321","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"258_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla PA, Jonsson B (1996) Verifying programs with unreliable channels. Inf Comput 127(2):91\u2013101","journal-title":"Inf Comput"},{"key":"258_CR4","doi-asserted-by":"publisher","unstructured":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H (2014) Parameterized model checking of rendezvous systems. In: CONCUR \u201914 Proceedings of the 25th International Conference on Concurrency Theory, vol 704 of LNCS. Springer, Heidelberg, pp 109\u2013124","DOI":"10.1007\/978-3-662-44584-6_9"},{"issue":"4","key":"258_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00446-007-0040-2","volume":"20","author":"D Angluin","year":"2007","unstructured":"Angluin D, Aspnes J, Eisenstat D, Ruppert E (2007) The computational power of population protocols. Distrib Comput 20(4):279\u2013304","journal-title":"Distrib Comput"},{"issue":"6","key":"258_CR6","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt KR, Kozen DC (1986) Limits for automatic verification of finite-state concurrent systems. Inf Process Lett 22(6):307\u2013309","journal-title":"Inf Process Lett"},{"key":"258_CR7","doi-asserted-by":"publisher","unstructured":"Bouajjani A, Esparza J, Maler O (1997) Reachability analysis of pushdown automata: application to model-checking. In: CONCUR \u201997 Proceedings of the 8th International Conference on Concurrency Theory, vol 1243 of LNCS. Springer, Heidelberg, pp 135\u2013150","DOI":"10.1007\/3-540-63141-0_10"},{"key":"258_CR8","doi-asserted-by":"publisher","unstructured":"Esparza J, Finkel A and Mayr R (1999) On the verification of broadcast protocols. In: LICS \u201999, IEEE Computer Society, Washington, DC, pp 352\u2013359","DOI":"10.1109\/LICS.1999.782630"},{"key":"258_CR9","doi-asserted-by":"publisher","unstructured":"Esparza J, Ganty P, Majumdar R (2013) Parameterized verification of asynchronous shared-memory systems. In: CAV \u201913 Proceedings of the 23rd International Conference on Computer Aided Verification, vol 8044 of LNCS. Springer, Heidelberg, pp 124\u2013140","DOI":"10.1007\/978-3-642-39799-8_8"},{"issue":"1","key":"258_CR10","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/2842603","volume":"63","author":"J Esparza","year":"2016","unstructured":"Esparza J, Ganty P, Majumdar R (2016) Parameterized verification of asynchronous shared-memory systems. J ACM 63(1):10","journal-title":"J ACM"},{"issue":"3","key":"258_CR11","doi-asserted-by":"publisher","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":"258_CR12","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1016\/0304-3975(88)90136-3","volume":"56","author":"E Gr\u00e4del","year":"1988","unstructured":"Gr\u00e4del E (1988) Subclasses of presburger arithmetic and the polynomial-time hierarchy. Theor Comput Sci 56:289\u2013301","journal-title":"Theor Comput Sci"},{"key":"258_CR13","unstructured":"Hague M (2011) Parameterised pushdown systems with non-atomic writes. In: Proceedings of FSTTCS \u201911, vol 13 of LIPIcs. Schloss Dagstuhl, Wadern, pp 457\u2013468"},{"key":"258_CR14","unstructured":"Meyer R (2008) On boundedness in depth in the pi-calculus. In: Proceedings of IFIP TCS 2008, vol 273 of IFIP. Springer, Heidelberg, pp 477\u2013489"},{"key":"258_CR15","unstructured":"Pnueli A, Xu J, Zuck LD (2002) Liveness with (0, 1, infty)-counter abstraction. In: CAV \u201902 Proceedings of 14th International Conference on Computer Aided Verification, vol 2404 of LNCS. Springer, Heidelberg, pp 107\u2013122"},{"key":"258_CR16","unstructured":"Torre SL, Muscholl A, Walukiewicz I (2015) Safety of parametrized asynchronous shared-memory systems is almost always decidable. In: CONCUR \u201915 Proceedings of 26th International Conference on Concurrency Theory, vol 42 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Wadern, pp 72\u201384"},{"key":"258_CR17","doi-asserted-by":"publisher","unstructured":"Verma KN, Seidl H, Schwentick T (2005) On the complexity of equational horn clauses. In: CADE \u201905 20th International Conference on Automated Deduction, vol 1831 of LNCS. Springer, Heidelberg, pp 337\u2013352","DOI":"10.1007\/11532231_25"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0258-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0258-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0258-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T11:37:36Z","timestamp":1492688256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0258-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,24]]},"references-count":17,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["258"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0258-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,24]]}}}