{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:09:12Z","timestamp":1767773352817,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":14,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,10]],"date-time":"2022-10-10T00:00:00Z","timestamp":1665360000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100017142","name":"Gruppo Nazionale per il Calcolo Scientifico","doi-asserted-by":"publisher","award":["Bando Visitatore"],"award-info":[{"award-number":["Bando Visitatore"]}],"id":[{"id":"10.13039\/100017142","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,10]]},"DOI":"10.1145\/3551349.3559523","type":"proceedings-article","created":{"date-parts":[[2023,1,5]],"date-time":"2023-01-05T20:43:54Z","timestamp":1672951434000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["CBMC-SSM: Bounded Model Checking of C\u00a0Programs with Symbolic Shadow Memory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1815-218X","authenticated-orcid":false,"given":"Bernd","family":"Fischer","sequence":"first","affiliation":[{"name":"Stellenbosch University, South Africa"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4978-4307","authenticated-orcid":false,"given":"Salvatore","family":"La Torre","sequence":"additional","affiliation":[{"name":"University of Salerno, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8697-2980","authenticated-orcid":false,"given":"Gennaro","family":"Parlato","sequence":"additional","affiliation":[{"name":"University of Molise, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5713-1381","authenticated-orcid":false,"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[{"name":"University of Sussex and Diffblue Ltd, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2023,1,5]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"216","volume-title":"USENIX Security Symp.","author":"Sys","unstructured":"[1] F., D., and D.\u00a0R.. Sys: A static\/symbolic tool for finding good bugs in good (browser) code. USENIX Security Symp., pp.99\u2013216. USENIX Assoc., 2020."},{"first-page":"224","volume-title":"OSDI","key":"e_1_3_2_1_2_1","unstructured":"[2] C., D., and D.\u00a0R.. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI, pp.09\u2013224. USENIX Assoc., 2008."},{"key":"e_1_3_2_1_3_1","first-page":"68","article-title":"A tool for checking ANSI-C programs. TACAS","year":"2004","unstructured":"[3] E.\u00a0M., D., and F.. A tool for checking ANSI-C programs. TACAS, LNCS\u00a02988, pp.68\u2013176, 2004.","journal-title":"LNCS\u00a02988"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_5_1","first-page":"812","volume-title":"ASE","author":"La Torre G..","unstructured":"[5] O., T.\u00a0L., B., S.{La Torre, and G.. Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. ASE, pp.07\u2013812. IEEE Comp.., 2015."},{"key":"e_1_3_2_1_6_1","first-page":"85","article-title":"Bounded model checking of multi-threaded C programs via lazy sequentialization. CAV","author":"La Torre G.","year":"2014","unstructured":"[6] O., E., B., S.{La Torre, and G.. Bounded model checking of multi-threaded C programs via lazy sequentialization. CAV, LNCS\u00a08559, pp.85\u2013602. Springer, 2014.","journal-title":"LNCS\u00a08559"},{"volume-title":"Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software","year":"2005","key":"e_1_3_2_1_7_1","unstructured":"[7] J.and D.\u00a0X.. Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software. NDSS. The Internet Society, 2005."},{"first-page":"64","volume-title":"USENIX Security Symp.","key":"e_1_3_2_1_8_1","unstructured":"[8] D.\u00a0A.and D.\u00a0R.. Under-constrained symbolic execution: Correctness checking for real code. USENIX Security Symp., pp.9\u201364. USENIX Assoc., 2015."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/265924.265927"},{"key":"e_1_3_2_1_10_1","first-page":"76","article-title":"Symbolic partial-order execution for testing multi-threaded programs. CAV","author":"\u00fcning C.","year":"2020","unstructured":"[10] D., J.\u00fcning, C.\u00edguez, D., and K.. Symbolic partial-order execution for testing multi-threaded programs. CAV, LNCS\u00a012224, pp.76\u2013400. Springer, 2020.","journal-title":"LNCS\u00a012224"},{"key":"e_1_3_2_1_11_1","first-page":"110","article-title":"Dynamic race detection with LLVM compiler - compile-time instrumentation for ThreadSanitizer. Runtime Verification","year":"2011","unstructured":"[11] K., A., T., and D.. Dynamic race detection with LLVM compiler - compile-time instrumentation for ThreadSanitizer. Runtime Verification, LNCS\u00a07168, pp. 110\u2013114. Springer, 2011.","journal-title":"LNCS\u00a07168"},{"volume-title":"Worksh.Software Verification. USENIX Assoc.","year":"2010","key":"e_1_3_2_1_12_1","unstructured":"[12] C., S., and F.. A precise memory model for low-level bounded model checking. Worksh.Software Verification. USENIX Assoc., 2010."},{"key":"e_1_3_2_1_13_1","first-page":"200","volume-title":"FMCAD","author":"Nguyen O., B., S.","unstructured":"[13] E., T.\u00a0L. Nguyen, O., B., S.{La Torre, and G.. Lazy sequentialization for TSO and PSO via shared memory abstractions. FMCAD, pp.93\u2013200. IEEE, 2016."},{"key":"e_1_3_2_1_14_1","first-page":"85","article-title":"Using shared memory abstractions to design eager sequentializations for weak memory models. SEFM","author":"Nguyen O., B., S.","year":"2017","unstructured":"[14] E., T.\u00a0L. Nguyen, O., B., S.{La Torre, and G.. Using shared memory abstractions to design eager sequentializations for weak memory models. SEFM, LNCS\u00a010469, pp.85\u2013202. Springer, 2017.","journal-title":"LNCS\u00a010469"}],"event":{"name":"ASE '22: 37th IEEE\/ACM International Conference on Automated Software Engineering","acronym":"ASE '22","location":"Rochester MI USA"},"container-title":["Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551349.3559523","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551349.3559523","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T08:31:36Z","timestamp":1755851496000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551349.3559523"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,10]]},"references-count":14,"alternative-id":["10.1145\/3551349.3559523","10.1145\/3551349"],"URL":"https:\/\/doi.org\/10.1145\/3551349.3559523","relation":{},"subject":[],"published":{"date-parts":[[2022,10,10]]},"assertion":[{"value":"2023-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}