{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:57Z","timestamp":1767929517675,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Deutsche Forschungsgemeinschaft","award":["389792660 TRR 248--CPEC"],"award-info":[{"award-number":["389792660 TRR 248--CPEC"]}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Grant Agreement 610150"],"award-info":[{"award-number":["Grant Agreement 610150"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            A fundamental problem in refinement verification is to check that the language of behaviors of an implementation is included in the language of the specification. We consider the refinement verification problem where the implementation is a multithreaded shared memory system modeled as a multistack pushdown automaton and the specification is an input-deterministic multistack pushdown language. Our main result shows that the\n            <jats:italic>context-bounded<\/jats:italic>\n            refinement problem, where we ask that all behaviors generated in runs of bounded number of context switches belong to a specification given by a Dyck language, is decidable and coNP-complete. The more general case of input-deterministic languages follows, with the same complexity. Context-bounding is essential since emptiness for multipushdown automata is already undecidable, and so is the refinement verification problem for the subclass of regular specifications. Input-deterministic languages capture many non-regular specifications of practical interest and our result opens the way for algorithmic analysis of these properties. The context-bounded refinement problem is coNP-hard already with deterministic regular specifications; our result demonstrates that the problem is not harder despite the stronger class of specifications. Our proof introduces several general techniques for formal languages and counter programs and shows that the search for counterexamples can be reduced in non-deterministic polynomial time to the satisfiability problem for existential Presburger arithmetic. These techniques are essential to ensure the coNP upper bound: existing techniques for regular specifications are not powerful enough for decidability, while simple reductions lead to problems that are either undecidable or have high complexities. As a special case, our decidability result gives an algorithmic verification technique to reason about reference counting and re-entrant locking in multithreaded programs.\n          <\/jats:p>","DOI":"10.1145\/3571266","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"2141-2170","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Context-Bounded Verification of Context-Free Specifications"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9371-0807","authenticated-orcid":false,"given":"Pascal","family":"Baumann","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0775-7781","authenticated-orcid":false,"given":"Moses","family":"Ganardi","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2039346.2039347"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007390"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516518"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2020.111"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434325"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-002-0085-4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111008040"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3464794"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1976-0396605-3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_30"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2020.106079"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434298"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2018.05.002"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90074-8"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322224"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3478536"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90564-5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.09.035"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12200-2_10"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_27_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 282\u2013298","author":"Lal Akash","year":"2008","unstructured":"Akash Lal , Tayssir Touili , Nicholas Kidd , and Thomas Reps . 2008 . Interprocedural Analysis of Concurrent Programs under a Context Bound . In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 282\u2013298 . Akash Lal, Tayssir Touili, Nicholas Kidd, and Thomas Reps. 2008. Interprocedural Analysis of Concurrent Programs under a Context Bound. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 282\u2013298."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785796"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_26"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-62822-2_6"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/322017.322031"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054121420077"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1515\/gcc-2012-0016"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814304"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926419"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2018.01.002"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.12"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_74"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90016-0"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029833"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0049431"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(72)90205-7"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(70)90446-8"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_1_52_1","volume-title":"Polynomial-time word problems. Commentarii mathematici helvetici, 83, 4","author":"Schleimer Saul","year":"2008","unstructured":"Saul Schleimer . 2008. Polynomial-time word problems. Commentarii mathematici helvetici, 83, 4 ( 2008 ), 741\u2013765. Saul Schleimer. 2008. Polynomial-time word problems. Commentarii mathematici helvetici, 83, 4 (2008), 741\u2013765."},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"G\u00e9raud S\u00e9nizergues. 1997. The equivalence problem for deterministic pushdown automata is decidable. In International Colloquium on Automata Languages and Programming. 671\u2013681. \t\t\t\t  G\u00e9raud S\u00e9nizergues. 1997. The equivalence problem for deterministic pushdown automata is decidable. In International Colloquium on Automata Languages and Programming. 671\u2013681.","DOI":"10.1007\/3-540-63165-8_221"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.29"},{"key":"e_1_2_1_55_1","volume-title":"Introduction to the Theory of Computation","author":"Sipser Michael","unstructured":"Michael Sipser . 2012. Introduction to the Theory of Computation ( 3 rd ed.). Cengage Learning, Inc. Michael Sipser. 2012. Introduction to the Theory of Computation (3rd ed.). Cengage Learning, Inc.","edition":"3"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104588"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_25"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_25"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571266","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571266","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571266"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571266"],"URL":"https:\/\/doi.org\/10.1145\/3571266","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}