{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T04:41:38Z","timestamp":1773895298198,"version":"3.50.1"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,3,3]],"date-time":"2023-03-03T00:00:00Z","timestamp":1677801600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62072267, 62021002"],"award-info":[{"award-number":["62072267, 62021002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"National Key Research and Development Program of China","award":["2018YFB1308601"],"award-info":[{"award-number":["2018YFB1308601"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"<jats:p>Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread interleavings concisely. However, there is no dedicated decision procedure for solving partial-order constraints.<\/jats:p>\n          <jats:p>\n            In this article, we propose a novel\n            <jats:italic>ordering consistency theory<\/jats:italic>\n            for concurrent program verification that is applicable not only under sequential consistency, but also under the TSO and PSO weak memory models. We further develop an efficient theory solver, which checks consistency incrementally, generates minimal conflict clauses, and includes a custom propagation procedure. We have implemented our approach in a tool, called\n            <jats:sc>Zord<\/jats:sc>\n            , and have conducted extensive experiments on the\n            <jats:italic>SV-COMP 2020 ConcurrencySafety<\/jats:italic>\n            benchmarks. Our experimental results show a significant improvement over the state-of-the-art.\n          <\/jats:p>","DOI":"10.1145\/3579835","type":"journal-article","created":{"date-parts":[[2023,1,17]],"date-time":"2023-01-17T12:04:33Z","timestamp":1673957073000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models"],"prefix":"10.1145","volume":"45","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6135-7308","authenticated-orcid":false,"given":"Hongyu","family":"Fan","sequence":"first","affiliation":[{"name":"Tsinghua University, China, Key Laboratory for Information System Security, MoE, China, and Beijing National Research Center for Information Science and Technology, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3787-0144","authenticated-orcid":false,"given":"Zhihang","family":"Sun","sequence":"additional","affiliation":[{"name":"Tsinghua University, China, Key Laboratory for Information System Security, MoE, China, and Beijing National Research Center for Information Science and Technology, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4266-875X","authenticated-orcid":false,"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"Tsinghua University, China, Key Laboratory for Information System Security, MoE, China, and Beijing National Research Center for Information Science and Technology, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77120-3_41"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1383369.1383370"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_33"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2756553"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_10"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"Ganzinger Harald","year":"2004","unstructured":"Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2004. DPLL(T): Fast decision procedures. In Computer Aided Verification, Rajeev Alur and Doron A. Peled (Eds.). Springer Berlin, 175\u2013188."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29778-1_18"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/2071379.2071382"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_3_2_34_2","unstructured":"Alex Horn and Jade Alglave. 2014. Concurrent Kleene Algebra of Partial Strings. arxiv:1407.0385 [cs.LO]."},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","unstructured":"Alex Horn and Daniel Kroening. 2015. On Partial Order Semantics for SAT\/SMT-based Symbolic Encodings of Weak Memory Concurrency. arxiv:1504.00037 [cs.LO].","DOI":"10.1007\/978-3-319-19195-9_2"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.108"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1159892.1159896"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(96)00075-0"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-17906-2_30","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"Mazurkiewicz Antoni","year":"1987","unstructured":"Antoni Mazurkiewicz. 1987. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, W. Brauer, W. Reisig, and G. Rozenberg (Eds.). Springer Berlin, 278\u2013324."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1187436.1210590"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.5555\/17634"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926433"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1971.10"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886679"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996713"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.5555\/174556"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_25"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238223"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2864122"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579835","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3579835","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:27Z","timestamp":1750182687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579835"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,3]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3579835"],"URL":"https:\/\/doi.org\/10.1145\/3579835","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,3,3]]},"assertion":[{"value":"2021-10-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-12-02","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}