{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T08:05:46Z","timestamp":1791273946731,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_8","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T23:13:06Z","timestamp":1373497986000},"page":"124-140","source":"Crossref","is-referenced-by-count":26,"title":["Parameterized Verification of Asynchronous Shared-Memory Systems"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","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","reference":[{"key":"8_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313\u2013321. IEEE Computer Society (1996)"},{"issue":"6","key":"8_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters\u00a022(6), 307\u2013309 (1986)","journal-title":"Information Processing Letters"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Arora, S., Barak, B.: Computational Complexity\u2013A Modern Approach. CUP (2009)","DOI":"10.1017\/CBO9780511804090"},{"issue":"56","key":"8_CR4","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1016\/S0019-9958(67)90771-1","volume":"11","author":"B. Brainerd","year":"1967","unstructured":"Brainerd, B.: An analog of a theorem about context-free languages. Information and Control\u00a011(56), 561\u2013567 (1967)","journal-title":"Information and Control"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G. Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design\u00a023(3), 257\u2013301 (2003)","journal-title":"Formal Methods in System Design"},{"key":"8_CR7","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., Raskin, J.-F., Van Begin, L.: Towards the automated verification of multithreaded java programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 173\u2013187. Springer, Heidelberg (2002)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-15375-4_22","volume-title":"CONCUR 2010 - Concurrency Theory","author":"G. Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 313\u2013327. Springer, Heidelberg (2010)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-78163-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Dimitrova","year":"2008","unstructured":"Dimitrova, R., Podelski, A.: Is lazy abstraction a decision procedure for broadcast protocols? In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 98\u2013111. Springer, Heidelberg (2008)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 247\u2013262. Springer, Heidelberg (2003)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/BFb0028766","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: Verification of parameterized bus arbitration protocol. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 452\u2013463. Springer, Heidelberg (1998)"},{"key":"8_CR12","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359. IEEE Computer Society (1999)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. CoRR abs\/1304.1185 (2013)","DOI":"10.1007\/978-3-642-39799-8_8"},{"key":"8_CR14","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":"8_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2160910.2160915","volume":"6","author":"P. Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst.\u00a06, 1\u20136 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"8_CR16","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/s00446-007-0042-0","volume":"20","author":"R. Guerraoui","year":"2007","unstructured":"Guerraoui, R., Ruppert, E.: Anonymous and fault-tolerant shared-memory computing. Distributed Computing\u00a020(3), 165\u2013177 (2007)","journal-title":"Distributed Computing"},{"key":"8_CR17","unstructured":"Hague, M.: Parameterised pushdown systems with non-atomic writes. In: Proc. of FSTTCS 2011. LIPIcs, vol.\u00a013, pp. 457\u2013468. Schloss Dagstuhl (2011)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Laaser, W.T.: Complete problems for deterministic polynomial time. In: Proc. of STOC 1974, pp. 40\u201346. ACM (1974)","DOI":"10.1145\/800119.803883"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A. Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 645\u2013659. Springer, Heidelberg (2010)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Laurendeau, C., Barbeau, M.: Secure anonymous broadcasting in vehicular networks. In: LCN 2007, pp. 661\u2013668. IEEE Computer Society (2007)","DOI":"10.1109\/LCN.2007.37"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of tomasulo\u2019s algorithm by compositional model checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 110\u2013121. Springer, Heidelberg (1998)"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/978-3-642-14295-6_54","volume-title":"Computer Aided Verification","author":"S. La Torre","year":"2010","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 629\u2013644. Springer, Heidelberg (2010)"},{"issue":"42","key":"8_CR23","doi-asserted-by":"publisher","first-page":"4169","DOI":"10.1016\/j.tcs.2009.01.021","volume":"410","author":"M. Viswanathan","year":"2009","unstructured":"Viswanathan, M., Chadha, R.: Deciding branching time properties for asynchronous programs. Theoretical Computer Science\u00a0410(42), 4169\u20134179 (2009)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T18:40:47Z","timestamp":1557945647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}