{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:32Z","timestamp":1759638812353,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,9,15]],"date-time":"2014-09-15T00:00:00Z","timestamp":1410739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,9,25]]},"abstract":"<jats:p>\n            Pattern-based verification checks the correctness of program executions that follow a given\n            <jats:italic>pattern<\/jats:italic>\n            , a regular expression over the alphabet of program transitions of the form\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            <jats:sup>*<\/jats:sup>\n            \u2026\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>\n              <jats:italic>n<\/jats:italic>\n            <\/jats:sub>\n            <jats:sup>*<\/jats:sup>\n            . For multithreaded programs, the alphabet of the pattern is given by the reads and writes to the shared storage. We study the complexity of pattern-based verification for multithreaded programs with shared counters and finite variables. While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs (even without counters), we show that pattern-based verification is NP-complete for both classes, even in the presence of counters. We then conduct a multiparameter analysis to study the complexity of the problem on its three natural parameters (number of threads+counters+variables, maximal size of a thread, size of the pattern) and on two parameters related to thread structure (maximal number of procedures per thread and longest simple path of procedure calls). We present an algorithm that for a fixed number of threads, counters, variables, and pattern size solves the verification problem in\n            <jats:italic>st<\/jats:italic>\n            <jats:sup>\n              <jats:italic>O<\/jats:italic>\n              (\n              <jats:italic>lsp<\/jats:italic>\n              + \u2308 log (\n              <jats:italic>pr<\/jats:italic>\n              +1) \u2309)\n            <\/jats:sup>\n            time, where\n            <jats:italic>st<\/jats:italic>\n            is the maximal size of a thread,\n            <jats:italic>pr<\/jats:italic>\n            is the maximal number of procedures per thread, and\n            <jats:italic>lsp<\/jats:italic>\n            is the longest simple path of procedure calls.\n          <\/jats:p>","DOI":"10.1145\/2629644","type":"journal-article","created":{"date-parts":[[2014,9,17]],"date-time":"2014-09-17T14:22:25Z","timestamp":1410963745000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Pattern-Based Verification for Multithreaded Programs"],"prefix":"10.1145","volume":"36","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[{"name":"Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Germany"}]},{"given":"Pierre","family":"Ganty","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Tom\u00e1\u0161","family":"Poch","sequence":"additional","affiliation":[{"name":"Charles University Prague, Faculty of Mathematics and Physics, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2014,9,15]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Zing: A Model Checker for Concurrent Software. Technical Report MSR-TR-2004-10. Microsoft Research.","author":"Andrews Tony","year":"2004","unstructured":"Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof, and Yichen Zie. 2004. Zing: A Model Checker for Concurrent Software. Technical Report MSR-TR-2004-10. Microsoft Research."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85780-8_9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(4:4)2011"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_29"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_36"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379396.2379398"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.03.019"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0136-y"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/578533"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1102023"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90028-3"},{"key":"e_1_2_1_12_1","unstructured":"Matthew Hague. 2011. Parameterised pushdown systems with non-atomic writes. In Proc. 31st IARCS Annual Conf. on Foundation of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics (LIPIcs)).Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik 457--468."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_22"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/574901"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.45"},{"key":"e_1_2_1_16_1","volume-title":"Tractable Dataflow Analysis for Concurrent Programs via Bounded Languages. (July","author":"Kahlon Vineet","year":"2009","unstructured":"Vineet Kahlon. 2009b. Tractable Dataflow Analysis for Concurrent Programs via Bounded Languages. (July 2009). Patent WO\/2009\/094439."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190262"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_49"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0078-9"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792761"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_25"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996845"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_19"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_36"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1978-0500555-0"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629644","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629644","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:30Z","timestamp":1750227210000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629644"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9,15]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,9,25]]}},"alternative-id":["10.1145\/2629644"],"URL":"https:\/\/doi.org\/10.1145\/2629644","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2014,9,15]]},"assertion":[{"value":"2012-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}