{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T14:18:36Z","timestamp":1766067516250,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T00:00:00Z","timestamp":1648425600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2018YFB1308601"],"award-info":[{"award-number":["2018YFB1308601"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100007162","name":"Guangdong Science and Technology Department","doi-asserted-by":"publisher","award":["2018B010107004"],"award-info":[{"award-number":["2018B010107004"]}],"id":[{"id":"10.13039\/501100007162","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62072267, 62021002"],"award-info":[{"award-number":["62072267, 62021002"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,4,2]]},"DOI":"10.1145\/3503221.3508424","type":"proceedings-article","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T13:58:22Z","timestamp":1648475902000},"page":"163-176","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Interference relation-guided SMT solving for multi-threaded program verification"],"prefix":"10.1145","author":[{"given":"Hongyu","family":"Fan","sequence":"first","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"given":"Weiting","family":"Liu","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}]}],"member":"320","published-online":{"date-parts":[[2022,3,28]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. Software Verification Competition Benchmarks. https:\/\/gitlab.com\/sosy-lab\/benchmarking\/sv-benchmarks\/-\/tree\/svcomp19\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_1_3_1","volume-title":"Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas.","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. CoRR abs\/1501.02069 (2015). arXiv:1501.02069"},{"key":"e_1_3_2_1_4_1","volume-title":"Bengt Jonsson, and Carl Leonardsson.","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 134--156."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"volume-title":"Partial Orders for Efficient Bounded Model Checking of Concurrent Software","author":"Alglave Jade","key":"e_1_3_2_1_6_1","unstructured":"Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 141--157."},{"volume-title":"Fences in Weak Memory Models","author":"Alglave Jade","key":"e_1_3_2_1_7_1","unstructured":"Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in Weak Memory Models. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 258--272."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","unstructured":"M. Berzish V. Ganesh and Y. Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In 2017 Formal Methods in Computer Aided Design (FMCAD). 55--59. 10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770423"},{"volume-title":"Logic for Programming","author":"Cassez Franck","key":"e_1_3_2_1_11_1","unstructured":"Franck Cassez and Frowin Ziegler. 2015. Verification of Concurrent Programs Using Trace Abstraction Refinement. In Logic for Programming, Artificial Intelligence, and Reasoning, Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 233--248."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996713"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238218"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","key":"e_1_3_2_1_19_1","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337--340."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_21_1","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010 - Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 - Object-Oriented Programming, Theo D'Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504--528."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_23_1","unstructured":"Jon W. Freeman. 1995. Improvements to propositional satisfiability search algorithms."},{"volume-title":"Fast Decision Procedures","author":"Ganzinger Harald","key":"e_1_3_2_1_24_1","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 Heidelberg, Berlin, Heidelberg, 175--188."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517437"},{"volume-title":"Proceedings of Design Automation Conference. 824--829","author":"Gupta A.","key":"e_1_3_2_1_27_1","unstructured":"A. Gupta, M. Ganai, Chao Wang, Zijiang Yang, and P. Ashar. 2003. Learning from BDDs in SAT-based bounded model checking. In Proceedings of Design Automation Conference. 824--829."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_3_2_1_30_1","volume-title":"Salvatore La Torre, and Gennaro Parlato","author":"Inverso Omar","year":"2014","unstructured":"Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 585--602."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.)","author":"Kroening Daniel","key":"e_1_3_2_1_33_1","unstructured":"Daniel Kroening and Michael Tautschnig. 2014. CBMC - C Bounded Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 389--391."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378470"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"volume-title":"Principles and Practice of Constraint Programming-CP97","author":"Li Chu Min","key":"e_1_3_2_1_37_1","unstructured":"Chu Min Li and Anbulagan. 1997. Look-ahead versus look-back for satisfiability problems. In Principles and Practice of Constraint Programming-CP97, Gert Smolka (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 341--355."},{"key":"e_1_3_2_1_38_1","volume-title":"Atulan Zaman, and Krzysztof Czarnecki.","author":"Liang Jia Hui","year":"2015","unstructured":"Jia Hui (Jimmy) Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. 2015. Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning, SAT Solvers. CoRR abs\/1506.08905 (2015). arXiv:1506.08905"},{"volume-title":"Progress in Artificial Intelligence, Pedro Barahona and Jos\u00e9 J","author":"Marques-Silva Jo\u00e3o","key":"e_1_3_2_1_39_1","unstructured":"Jo\u00e3o Marques-Silva. 1999. The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. In Progress in Artificial Intelligence, Pedro Barahona and Jos\u00e9 J. Alferes (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 62--74."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.769433"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379017"},{"volume-title":"Theorem Proving in Higher Order Logics","author":"Owens Scott","key":"e_1_3_2_1_43_1","unstructured":"Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 391--407."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926433"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"E. Tomasco T. L. Nguyen O. Inverso B. Fischer S. L. Torre and G. Parlato. 2016. Lazy sequentialization for TSO and PSO via shared memory abstractions. In 2016 Formal Methods in Computer-Aided Design (FMCAD). 193--200.","DOI":"10.1109\/FMCAD.2016.7886679"},{"key":"e_1_3_2_1_47_1","unstructured":"D. Weaver and Tom Gremond. 1994. The SPARC architecture manual: version 9."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238223"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00074"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2864122"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2013.11"}],"event":{"name":"PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGHPC ACM Special Interest Group on High Performance Computing, Special Interest Group on High Performance Computing"],"location":"Seoul Republic of Korea","acronym":"PPoPP '22"},"container-title":["Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3503221.3508424","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3503221.3508424","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:49Z","timestamp":1750186849000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3503221.3508424"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,28]]},"references-count":51,"alternative-id":["10.1145\/3503221.3508424","10.1145\/3503221"],"URL":"https:\/\/doi.org\/10.1145\/3503221.3508424","relation":{},"subject":[],"published":{"date-parts":[[2022,3,28]]},"assertion":[{"value":"2022-03-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}