{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T15:14:17Z","timestamp":1772032457833,"version":"3.50.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030670665","type":"print"},{"value":"9783030670672","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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-67067-2_7","type":"book-chapter","created":{"date-parts":[[2021,1,11]],"date-time":"2021-01-11T20:57:20Z","timestamp":1610398640000},"page":"127-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Self-certifying Compilation Framework for WebAssembly"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,12]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.D.: TVOC: a translation validator for optimizing compilers. In: CAV, pp. 291\u2013295 (2005)","DOI":"10.1007\/11513988_29"},{"issue":"1","key":"7_CR2","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/2579080","volume":"36","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Demange, D., Pichardie, D.: Formal verification of an SSA-based middle-end for CompCert. ACM Trans. Program. Lang. Syst. 36(1), 4 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14\u201325 (2004)","DOI":"10.1145\/982962.964003"},{"issue":"4","key":"7_CR4","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. J. Autom. Reasoning 5(4), 411\u2013428 (1989)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M Blum","year":"1995","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. J. ACM 42(1), 269\u2013291 (1995)","journal-title":"J. ACM"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: PLDI, pp. 1027\u20131040 (2019)","DOI":"10.1145\/3314221.3314596"},{"issue":"4","key":"7_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Dahiya, M., Bansal, S.: Modeling undefined behaviour semantics for checking equivalence across compiler optimizations. In: HVC, pp. 19\u201334 (2017)","DOI":"10.1007\/978-3-319-70389-3_2"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. In: Texts and Monographs in Computer Science, Springer, New York (1990). https:\/\/doi.org\/10.1007\/978-1-4612-3228-5","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-662-48899-7_42","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Automated discovery of simulation between\u00a0programs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 606\u2013621. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_42"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-662-46081-8_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Gjomemo","year":"2015","unstructured":"Gjomemo, R., Namjoshi, K.S., Phung, P.H., Venkatakrishnan, V.N., Zuck, L.D.: From verification to optimizations. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 300\u2013317. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_17"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Design Automation Conference, DAC 2009, San Francisco, CA, USA, July 26\u201331, 2009, pp. 466\u2013471 (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab. 23(3), 241\u2013258 (2013)","DOI":"10.1002\/stvr.1472"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Haas, A., et al.: Bringing the web up to speed with WebAssembly. In: PLDI, pp. 185\u2013200 (2017)","DOI":"10.1145\/3140587.3062363"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Jourdan, J., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: ESOP, pp. 397\u2013416 (2012)","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Kang, J., Kim, Y., et al.: Crellvm: verified credible compilation for LLVM. In: PLDI, pp. 631\u2013645 (2018)","DOI":"10.1145\/3296979.3192377"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: CAV, pp. 712\u2013717 (2012)","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"issue":"7","key":"7_CR19","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)","journal-title":"Commun. ACM"},{"key":"7_CR20","unstructured":"Marinov, D.: Credible Compilation. Master\u2019s thesis, Massachusetts Institute of Technology (2000)"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions, pp. 33\u201341. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: CAV, pp. 2\u201313 (2001)","DOI":"10.1007\/3-540-44585-4_2"},{"key":"7_CR24","unstructured":"Namjoshi, K.S.: Witnessing an SSA transformation. In: VeriSure Workshop, CAV (2014). https:\/\/kedar-namjoshi.github.io\/papers\/Namjoshi-VeriSure-CAV-2014.pdf"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S., Singhania, N.: Loopy: Programmable and formally verified loop transformations. In: SAS, pp. 383\u2013402 (2016)","DOI":"10.1007\/978-3-662-53413-7_19"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S., Tagliabue, G., Zuck, L.D.: A witnessing compiler: a proof of concept. In: RV, pp. 340\u2013345 (2013)","DOI":"10.1007\/978-3-642-40787-1_22"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-38856-9_17","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2013","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304\u2013323. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation of an optimizing compiler. In: (PLDI) 2000, pp. 83\u201395 (2000)","DOI":"10.1145\/349299.349314"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: FSTTCS, pp. 292\u2013304 (2001)","DOI":"10.1007\/3-540-45294-X_25"},{"issue":"2","key":"7_CR30","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT)- automatic verification of a compilation process. Software Tools Technol. Transfer 2(2), 192\u2013201 (1998)","journal-title":"Software Tools Technol. Transfer"},{"key":"7_CR31","unstructured":"Rinard, M.: Credible Compilation. Tech. Rep. MIT-LCS-TR-776, MIT (1999)"},{"key":"7_CR32","unstructured":"Samet, H.: Automatically proving the correctness of translations involving optimized code - research sponsored by Advanced Research Projects Agency, ARPA order no. 2494. Ph.D. thesis, Stanford University (1975)"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-319-48989-6_39","volume-title":"FM 2016: Formal Methods","author":"O Strichman","year":"2016","unstructured":"Strichman, O., Veitsman, M.: Regression verification for unbalanced recursive functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 645\u2013658. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_39"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Zaks, A., Pnueli, A.: Program analysis for compiler validation. In: PASTE, pp. 1\u20137 (2008)","DOI":"10.1145\/1512475.1512477"},{"key":"7_CR35","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880\u201310885 (2003)"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013, pp. 175\u2013186 (2013)","DOI":"10.1145\/2499370.2462164"},{"issue":"3","key":"7_CR37","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10703-005-3402-z","volume":"27","author":"LD Zuck","year":"2005","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B., Barrett, C.W., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Formal Methods Syst. Des. 27(3), 335\u2013360 (2005)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67067-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T20:10:27Z","timestamp":1718050227000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-67067-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030670665","9783030670672"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67067-2_7","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":"12 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Copenhagen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 January 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl21.sigplan.org\/home\/VMCAI-2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"48","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":"22","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":"1","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":"46% - 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,1","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":"4,6","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":"The conference took place virtually due to the COVID-19 pandemic.","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)"}}]}}