{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:02Z","timestamp":1776333482328,"version":"3.51.2"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030816872","type":"print"},{"value":"9783030816889","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Several automatic verification tools have been recently developed to verify subsets of LLVM\u2019s optimizations. However, none of these tools has robust support to verify memory optimizations.<\/jats:p><jats:p>In this paper, we present the first SMT encoding of LLVM\u2019s memory model that 1) is sufficiently precise to validate all of LLVM\u2019s intra-procedural memory optimizations, and 2) enables bounded translation validation of programs with up\u00a0to hundreds of thousands of lines of code. We implemented our new encoding in Alive2, a bounded translation validation tool, and used it to uncover 21 new bugs in LLVM memory optimizations, 10 of which have been already fixed. We also found several inconsistencies in LLVM IR\u2019s official specification document (LangRef) and fixed LLVM\u2019s code and the document so they are in agreement.<\/jats:p>","DOI":"10.1007\/978-3-030-81688-9_35","type":"book-chapter","created":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:20:47Z","timestamp":1626452447000},"page":"752-776","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["An SMT Encoding of LLVM\u2019s Memory Model for Bounded Translation Validation"],"prefix":"10.1007","author":[{"given":"Juneyoung","family":"Lee","sequence":"first","affiliation":[]},{"given":"Dongjoo","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[]},{"given":"Nuno P.","family":"Lopes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"35_CR1","unstructured":"LLVM language reference manual. https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"35_CR2","unstructured":"Ball, T., Bounimova, E., Levin, V., de Moura, L.: Efficient evaluation of pointer predicates with Z3 SMT solver in SLAM2. Technical Report MSR-TR-2010-24, Microsoft Research (2010), https:\/\/www.microsoft.com\/en-us\/research\/publication\/efficient-evaluation-of-pointer-predicates-with-z3-smt-solver-in-slam2\/"},{"key":"35_CR3","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: FMCO (2006). https:\/\/doi.org\/10.1007\/11804192_6","DOI":"10.1007\/11804192_6"},{"key":"35_CR4","doi-asserted-by":"publisher","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: Slayer: memory safety for systems-level code. In: CAV (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_15","DOI":"10.1007\/978-3-642-22110-1_15"},{"key":"35_CR5","doi-asserted-by":"publisher","unstructured":"Besson, F., Blazy, S., Wilke, P.: A concrete memory model for CompCert. In: ITP (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_5","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"35_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified horn clauses. In: SAS (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"35_CR7","doi-asserted-by":"publisher","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: CAV (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_7","DOI":"10.1007\/3-540-45657-0_7"},{"key":"35_CR8","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Vafeiadis, V.: Formalizing the concurrency semantics of an LLVM fragment. In: CGO (2017). https:\/\/doi.org\/10.1109\/CGO.2017.7863732","DOI":"10.1109\/CGO.2017.7863732"},{"key":"35_CR9","doi-asserted-by":"publisher","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"35_CR10","doi-asserted-by":"publisher","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: ASE (2009). https:\/\/doi.org\/10.1109\/ASE.2009.63","DOI":"10.1109\/ASE.2009.63"},{"key":"35_CR11","doi-asserted-by":"publisher","unstructured":"Dahiya, M., Bansal, S.: Black-box equivalence checking across compiler optimizations. In: APLAS (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_7","DOI":"10.1007\/978-3-319-71237-6_7"},{"key":"35_CR12","doi-asserted-by":"publisher","unstructured":"Dahiya, M., Bansal, S.: Modeling undefined behaviour semantics for checking equivalence across compiler optimizations. In: HVC (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_2","DOI":"10.1007\/978-3-319-70389-3_2"},{"key":"35_CR13","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"35_CR14","doi-asserted-by":"publisher","unstructured":"Gupta, S., Saxena, A., Mahajan, A., Bansal, S.: Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition. In: SAT (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_22","DOI":"10.1007\/978-3-319-94144-8_22"},{"key":"35_CR15","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Navas, J.A.: A context-sensitive memory model for verification of C\/C++ programs. In: SAS (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_8","DOI":"10.1007\/978-3-319-66706-5_8"},{"key":"35_CR16","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: SMT-friendly formalization of the solidity memory model. In: ESOP (2020)","DOI":"10.26226\/morressier.604907f41a80aac83ca25d57"},{"key":"35_CR17","doi-asserted-by":"publisher","unstructured":"Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: VMCAI (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_6","DOI":"10.1007\/978-3-030-39322-9_6"},{"issue":"6","key":"35_CR18","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1002\/spe.913","volume":"39","author":"A Kanade","year":"2009","unstructured":"Kanade, A., Sanyal, A., Khedker, U.P.: Validation of GCC optimizers through trace generation. SP&E 39(6), 611\u2013639 (2009). https:\/\/doi.org\/10.1002\/spe.913","journal-title":"SP&E"},{"key":"35_CR19","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integer-pointer casts. In: PLDI (2015). https:\/\/doi.org\/10.1145\/2737924.2738005","DOI":"10.1145\/2737924.2738005"},{"key":"35_CR20","doi-asserted-by":"publisher","unstructured":"Kang, J., et al.: Crellvm: Verified credible compilation for LLVM. In: PLDI (2018). https:\/\/doi.org\/10.1145\/3192366.3192377","DOI":"10.1145\/3192366.3192377"},{"issue":"3","key":"35_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10703-017-0293-8","volume":"52","author":"V Klebanov","year":"2018","unstructured":"Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification of pointer programs by predicate abstraction. Formal Methods Syst. Des. 52(3), 229\u2013259 (2018). https:\/\/doi.org\/10.1007\/s10703-017-0293-8","journal-title":"Formal Methods Syst. Des."},{"key":"35_CR22","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using horn clauses over integers and arrays. In: FMCAD (2015). https:\/\/doi.org\/10.1109\/FMCAD.2015.7542257","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"35_CR23","doi-asserted-by":"publisher","unstructured":"Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: PLDI (2014). https:\/\/doi.org\/10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"35_CR24","doi-asserted-by":"publisher","unstructured":"Lee, J., Hur, C.K., Jung, R., Liu, Z., Regehr, J., Lopes, N.P.: Reconciling high-level optimizations and low-level code in LLVM. In: Proceedings of the ACM on Programming Languages 2(OOPSLA), November 2018. https:\/\/doi.org\/10.1145\/3276495","DOI":"10.1145\/3276495"},{"key":"35_CR25","doi-asserted-by":"publisher","unstructured":"Lee, J., Hur, C.K., Lopes, N.P.: AliveInLean: a verified LLVM peephole optimization verifier. In: CAV (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_25","DOI":"10.1007\/978-3-030-25543-5_25"},{"key":"35_CR26","doi-asserted-by":"publisher","unstructured":"Lee, J., et al.: Taming undefined behavior in LLVM. In: PLDI (2017). https:\/\/doi.org\/10.1145\/3062341.3062343","DOI":"10.1145\/3062341.3062343"},{"issue":"7","key":"35_CR27","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"35_CR28","unstructured":"d Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model, version 2. Technical Report RR-7987, INRIA, June 2012. http:\/\/hal.inria.fr\/hal-00703441"},{"key":"35_CR29","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.7","author":"L Li","year":"2020","unstructured":"Li, L., Gunter, E.L.: -LLVM: a relatively complete semantics of LLVM IR. ECOOP (2020). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2020.7","journal-title":"ECOOP"},{"key":"35_CR30","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Lee, J., Hur, C.K., Liu, Z., Regehr, J.: Alive2: bounded translation validation for LLVM. In: PLDI (2021). https:\/\/doi.org\/10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"35_CR31","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with Alive. In: PLDI (2015). https:\/\/doi.org\/10.1145\/2737924.2737965","DOI":"10.1145\/2737924.2737965"},{"key":"35_CR32","doi-asserted-by":"publisher","unstructured":"Memarian, K., et al.: Exploring C semantics and pointer provenance. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290380","DOI":"10.1145\/3290380"},{"key":"35_CR33","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"35_CR34","doi-asserted-by":"publisher","unstructured":"Mullen, E., Zuniga, D., Tatlock, Z., Grossman, D.: Verified peephole optimizations for CompCert. In: PLDI (2016). https:\/\/doi.org\/10.1145\/2908080.2908109","DOI":"10.1145\/2908080.2908109"},{"key":"35_CR35","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S., Tagliabue, G., Zuck, L.D.: A witnessing compiler: a proof of concept. In: RV (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_22","DOI":"10.1007\/978-3-642-40787-1_22"},{"key":"35_CR36","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: SAS (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"35_CR37","doi-asserted-by":"publisher","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: APLAS (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_7","DOI":"10.1007\/978-3-319-03542-0_7"},{"key":"35_CR38","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000). https:\/\/doi.org\/10.1145\/349299.349314","DOI":"10.1145\/349299.349314"},{"key":"35_CR39","doi-asserted-by":"publisher","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: CAV (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_54","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"35_CR40","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: TACAS (1998). https:\/\/doi.org\/10.1007\/BFb0054170","DOI":"10.1007\/BFb0054170"},{"key":"35_CR41","unstructured":"Rinard, M.C., Marinov, D.: Credible compilation with pointers. In: RTRV (1999)"},{"key":"35_CR42","doi-asserted-by":"publisher","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: CAV (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-159","DOI":"10.1007\/978-3-642-22110-159"},{"key":"35_CR43","doi-asserted-by":"publisher","unstructured":"Torlak, E., Vaziri, M., Dolby, J.: MemSAT: checking axiomatic specifications of memory models. In: PLDI (2010). https:\/\/doi.org\/10.1145\/1806596.1806635","DOI":"10.1145\/1806596.1806635"},{"key":"35_CR44","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., Govereau, P., Morrisett, J.G.: Evaluating value-graph translation validation for LLVM. In: PLDI (2011). https:\/\/doi.org\/10.1145\/1993316.1993533","DOI":"10.1145\/1993316.1993533"},{"key":"35_CR45","doi-asserted-by":"publisher","unstructured":"Wang, W., Barrett, C., Wies, T.: Partitioned memory models for program analysis. In: VMCAI (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_29","DOI":"10.1007\/978-3-319-52234-0_29"},{"key":"35_CR46","doi-asserted-by":"publisher","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI (2011). https:\/\/doi.org\/10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"35_CR47","doi-asserted-by":"publisher","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL (2012). https:\/\/doi.org\/10.1145\/2103656.2103709","DOI":"10.1145\/2103656.2103709"},{"key":"35_CR48","doi-asserted-by":"publisher","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI (2013). https:\/\/doi.org\/10.1145\/2491956.2462164","DOI":"10.1145\/2491956.2462164"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81688-9_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,16]],"date-time":"2021-07-16T16:29:28Z","timestamp":1626452968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81688-9_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816872","9783030816889"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81688-9_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"63","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}