{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:15Z","timestamp":1750220655522,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T00:00:00Z","timestamp":1607299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA MUSE","award":["FA8750-14-2-0270"],"award-info":[{"award-number":["FA8750-14-2-0270"]}]},{"DOI":"10.13039\/100000006","name":"Naval Research","doi-asserted-by":"crossref","award":["N00014-17-1-2889 and N00014-19-1-2318"],"award-info":[{"award-number":["N00014-17-1-2889 and N00014-19-1-2318"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"U.S. National Science Foundation","doi-asserted-by":"crossref","award":["1253331"],"award-info":[{"award-number":["1253331"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"crossref"}]},{"name":"DARPA STAC","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,12,31]]},"abstract":"<jats:p>A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch \u201cmost bugs\u201d in practice, as errors tend to occur within few contexts. The question of whether the technique can also prove the absence of bugs at least in some cases has remained largely open.<\/jats:p>\n          <jats:p>\n            Toward closing this gap, we introduce in this article the generic verification paradigm of\n            <jats:italic>observation sequences<\/jats:italic>\n            for resource-parameterized programs. Such a sequence observes how increasing the resource parameter affects the reachability of states satisfying a given property. The goal is to show that increases beyond some \u201ccutoff\u201d parameter value have no impact on the reachability\u2014the sequence has\n            <jats:italic>converged<\/jats:italic>\n            . This allows us to conclude that the property holds for all parameter values.\n          <\/jats:p>\n          <jats:p>\n            We applied this paradigm to the context-\n            <jats:italic>unbounded<\/jats:italic>\n            program analysis problem, choosing the resource to be the number of permitted thread context switches. The result is a partially correct interprocedural reachability analysis technique for concurrent shared-memory programs. Our technique may not terminate but is able to both refute and prove context-unbounded safety for such programs. We demonstrate the effectiveness and efficiency of the technique using a variety of benchmark programs. The safe instances cannot be proved safe by earlier, context-bounded methods.\n          <\/jats:p>","DOI":"10.1145\/3418583","type":"journal-article","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T18:11:40Z","timestamp":1607364700000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Interprocedural Context-Unbounded Program Analysis Using Observation Sequences"],"prefix":"10.1145","volume":"42","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3583-457X","authenticated-orcid":false,"given":"Peizun","family":"Liu","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, MA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin\u2013Madison and GrammaTech Inc."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,12,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0406-x"},{"volume-title":"Proceedings of the 36th Annual ACM Symposium on Theory of Computing (STOC\u201904)","author":"Alur Rajeev","key":"e_1_2_1_2_1","unstructured":"Rajeev Alur and P. Madhusudan. 2004. Visibly pushdown languages. In Proceedings of the 36th Annual ACM Symposium on Theory of Computing (STOC\u201904). ACM, New York, NY, 202--211. http:\/\/doi.acm.org\/10.1145\/1007352.1007390"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1516512.1516518"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_11"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_7"},{"key":"e_1_2_1_7_1","volume-title":"Retrieved","author":"Beyer Dirk","year":"2019","unstructured":"Dirk Beyer. 2019. Sv-benchmarks. Retrieved October 16, 2020 from https:\/\/github.com\/sosy-lab\/sv-benchmarks\/tree\/master\/clauses\/BOOL."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.045"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-016-9700-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041565"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646732.701281"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_28"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770383"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_36"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054196000191"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/648236.753642"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16164-3_17"},{"volume-title":"Introduction to Automata Theory, Languages and Computation","author":"Hopcroft John","key":"e_1_2_1_22_1","unstructured":"John Hopcroft and Jeffrey Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190262"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_49"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_1_27_1","first-page":"2","article-title":"\u00dcber eine Schlussweise aus dem Endlichen ins Unendliche (in German). Acta Sci","volume":"3","author":"K\u00f6nig D\u00e9nes","year":"1927","unstructured":"D\u00e9nes K\u00f6nig. 1927. \u00dcber eine Schlussweise aus dem Endlichen ins Unendliche (in German). Acta Sci. Math. (Szeged) 3, 2\u20133, 121--130.","journal-title":"Math. (Szeged)"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/320613.320619"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.9"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792762"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_54"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2040235.2040253"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054116400074"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542500"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192419"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.17760\/D20328155"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_22"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346323"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_45"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_12"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964022"},{"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\/349214.349241"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_19"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3418583","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3418583","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3418583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:28Z","timestamp":1750197748000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3418583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,7]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,12,31]]}},"alternative-id":["10.1145\/3418583"],"URL":"https:\/\/doi.org\/10.1145\/3418583","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2020,12,7]]},"assertion":[{"value":"2019-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}