{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:31Z","timestamp":1775868451599,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T00:00:00Z","timestamp":1704758400000},"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":[],"published-print":{"date-parts":[[2024,1,9]]},"DOI":"10.1145\/3636501.3636940","type":"proceedings-article","created":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T19:39:27Z","timestamp":1704829167000},"page":"60-74","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Compositional Verification of Concurrent C Programs with Search Structure Templates"],"prefix":"10.1145","author":[{"given":"Duc-Than","family":"Nguyen","sequence":"first","affiliation":[{"name":"University of Illinois at Chicago, Chicago, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lennart","family":"Beringer","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"Mansky","sequence":"additional","affiliation":[{"name":"University of Illinois at Chicago, Chicago, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyi","family":"Wang","sequence":"additional","affiliation":[{"name":"Princeton University, Princeton, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press. isbn:110704801X"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_2_1_3_1","volume-title":"TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg","author":"da Rocha Pinto Pedro","year":"2014","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 207\u2013231. isbn:978-3-662-44202-9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428196"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_10_1","volume-title":"Compositional Abstractions for Verifying Concurrent Data Structures. Ph. D. Dissertation","author":"Krishna Siddharth","unstructured":"Siddharth Krishna. 2019. Compositional Abstractions for Verifying Concurrent Data Structures. Ph. D. Dissertation. New York University."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2207.06574"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168855"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Duc-Than Nguyen Lennart Beringer William Mansky and Shengyi Wang. 2023. Compositional Verification of Concurrent C Programs with Search Structure Templates (Artifact). https:\/\/doi.org\/10.5281\/zenodo.8337004 10.5281\/zenodo.8337004","DOI":"10.5281\/zenodo.8337004"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485490"},{"key":"e_1_3_2_1_18_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.)","author":"Piskac Ruzica","unstructured":"Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. GRASShopper. In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 124\u2013139. isbn:978-3-642-54862-8"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_3_2_1_20_1","unstructured":"Roshan Sharma Shengyi Wang Alexander Oey Anastasiia Evdokimova Lennart Beringer and William Mansky. 2022. Proving Logical Atomicity using Lock Invariants. Presented at Advances in Separation Logic (ASL 2022)"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/42201.42204"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503689"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303955"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_36"}],"event":{"name":"CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"London UK","acronym":"CPP '24","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636940","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3636501.3636940","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:11Z","timestamp":1750287251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3636501.3636940"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,9]]},"references-count":25,"alternative-id":["10.1145\/3636501.3636940","10.1145\/3636501"],"URL":"https:\/\/doi.org\/10.1145\/3636501.3636940","relation":{},"subject":[],"published":{"date-parts":[[2024,1,9]]},"assertion":[{"value":"2024-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}