{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:20:37Z","timestamp":1750220437031,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,17]],"date-time":"2021-01-17T00:00:00Z","timestamp":1610841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"name":"European Union?s Horizon 2020 research and innovation program","award":["830927"],"award-info":[{"award-number":["830927"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,1,17]]},"DOI":"10.1145\/3437992.3439923","type":"proceedings-article","created":{"date-parts":[[2021,1,20]],"date-time":"2021-01-20T23:11:11Z","timestamp":1611184271000},"page":"61-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards efficient and verified virtual machines for dynamic languages"],"prefix":"10.1145","author":[{"given":"Martin","family":"Desharnais","sequence":"first","affiliation":[{"name":"Bundeswehr University Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Brunthaler","sequence":"additional","affiliation":[{"name":"Bundeswehr University Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,20]]},"reference":[{"volume-title":"Retrieved February 18th","year":"2011","author":"Anand S.","key":"e_1_3_2_1_1_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"John Aycock. 2003. A brief history of just-in-time. Comput. Surveys 35 2 ( 2003 ) 97-113. htps:\/\/doi.org\/10.1145\/857076.857077  John Aycock. 2003. A brief history of just-in-time. Comput. Surveys 35 2 ( 2003 ) 97-113. htps:\/\/doi.org\/10.1145\/857076.857077","DOI":"10.1145\/857076.857077"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Sandrine Blazy Zaynah Dargaye and Xavier Leroy. 2006. Formal Verification of a C Compiler Front-End. 460-475. htps:\/\/doi.org\/10. 1007\/11813040_31  Sandrine Blazy Zaynah Dargaye and Xavier Leroy. 2006. Formal Verification of a C Compiler Front-End. 460-475. htps:\/\/doi.org\/10. 1007\/11813040_31","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Stefan Brunthaler. 2009. Virtual-Machine Abstraction and Optimization Techniques. Electronic Notes in Theoretical Computer Science 253 5 ( 2009 ) 3-14.  Stefan Brunthaler. 2009. Virtual-Machine Abstraction and Optimization Techniques. Electronic Notes in Theoretical Computer Science 253 5 ( 2009 ) 3-14.","DOI":"10.1016\/j.entcs.2009.11.011"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Stefan Brunthaler. 2010. Eficient interpretation using quickening.  Stefan Brunthaler. 2010. Eficient interpretation using quickening.","DOI":"10.1145\/1869631.1869633"},{"volume-title":"Inline caching meets quickening","series-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","author":"Brunthaler Stefan","key":"e_1_3_2_1_9_1"},{"key":"e_1_3_2_1_10_1","unstructured":"Martin Desharnais. 2020. A Generic Framework for Verified Compilers. Archive of Formal Proofs (Feb. 2020 ). htps:\/\/isa-afp.org\/entries\/ VeriComp.html Formal proof development.  Martin Desharnais. 2020. A Generic Framework for Verified Compilers. Archive of Formal Proofs (Feb. 2020 ). htps:\/\/isa-afp.org\/entries\/ VeriComp.html Formal proof development."},{"key":"e_1_3_2_1_11_1","unstructured":"Martin Desharnais. 2020. Inline Caching and Unboxing Optimization for Interpreters. Archive of Formal Proofs (Dec. 2020 ). htps:\/\/isaafp.org\/entries\/Interpreter_Optimizations.html Formal proof development.  Martin Desharnais. 2020. Inline Caching and Unboxing Optimization for Interpreters. Archive of Formal Proofs (Dec. 2020 ). htps:\/\/isaafp.org\/entries\/Interpreter_Optimizations.html Formal proof development."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800542"},{"key":"e_1_3_2_1_13_1","unstructured":"M Anton Ertl and David Gregg. 2003. The Structure and Performance of Eficient Interpreters. Journal of Instruction-Level Parallelism 5 (nov 2003 ) 1-25.  M Anton Ertl and David Gregg. 2003. The Structure and Performance of Eficient Interpreters. Journal of Instruction-Level Parallelism 5 (nov 2003 ) 1-25."},{"volume-title":"Proc. ACM Program. Lang. 2, POPL, Article 49 (","year":"2017","author":"Fl\u00fcckiger Olivier","key":"e_1_3_2_1_14_1"},{"volume-title":"Retrieved April 25th","year":"2013","author":"Fulgham Brent","key":"e_1_3_2_1_15_1"},{"key":"e_1_3_2_1_16_1","unstructured":"Sabine Glesner G. Goos F. v. Henke H. Langmaack W. Goerigk and W. Zimmermann. 2004. Abschlussbericht Verifix. Technical Report. Universit\u00e4ten Karlsruhe Kiel Ulm.  Sabine Glesner G. Goos F. v. Henke H. Langmaack W. Goerigk and W. Zimmermann. 2004. Abschlussbericht Verifix. Technical Report. Universit\u00e4ten Karlsruhe Kiel Ulm."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_10"},{"key":"e_1_3_2_1_18_1","unstructured":"Samuel Gro\u00df. 2020. JITSploitation I: A JIT Bug. htps:\/\/ googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-one. html Accessed: 2020-09-21.  Samuel Gro\u00df. 2020. JITSploitation I: A JIT Bug. htps:\/\/ googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-one. html Accessed: 2020-09-21."},{"key":"e_1_3_2_1_19_1","unstructured":"Samuel Gro\u00df. 2020. JITSploitation II : Getting Read\/Write. htps: \/\/googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-two. html Accessed: 2020-09-21.  Samuel Gro\u00df. 2020. JITSploitation II : Getting Read\/Write. htps: \/\/googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-two. html Accessed: 2020-09-21."},{"key":"e_1_3_2_1_20_1","unstructured":"Samuel Gro\u00df. 2020. JITSploitation III: Subverting Control Flow. htps:\/\/ googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-three. html Accessed: 2020-09-21.  Samuel Gro\u00df. 2020. JITSploitation III: Subverting Control Flow. htps:\/\/ googleprojectzero.blogspot.com\/ 2020 \/09\/jitsploitation-three. html Accessed: 2020-09-21."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The Essence of JavaScript. 126-150. htps:\/\/doi.org\/10.1007\/978-3-642-14107-2_7  Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The Essence of JavaScript. 126-150. htps:\/\/doi.org\/10.1007\/978-3-642-14107-2_7","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_3_2_1_22_1","unstructured":"Michael G. Hinchey Jonathan P. Bowen and Ernst-R\u00fcdiger Olderog (Eds.). 2017. Provably Correct Systems. Springer. htps:\/\/doi.org\/10. 1007\/978-3-319-48628-4  Michael G. Hinchey Jonathan P. Bowen and Ernst-R\u00fcdiger Olderog (Eds.). 2017. Provably Correct Systems. Springer. htps:\/\/doi.org\/10. 1007\/978-3-319-48628-4"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0057013"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178478"},{"volume-title":"Retrieved April 25th","year":"2012","key":"e_1_3_2_1_25_1"},{"volume-title":"Jinja is not Java. Archive of Formal Proofs (","year":"2005","author":"Klein Gerwin","key":"e_1_3_2_1_26_1"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025055424017"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_31_1","unstructured":"Andreas Lochbihler. 2007. Jinja with Threads. Archive of Formal Proofs (Dec. 2007 ). htps:\/\/isa-afp.org\/entries\/JinjaThreads.html Formal proof development.  Andreas Lochbihler. 2007. Jinja with Threads. Archive of Formal Proofs (Dec. 2007 ). htps:\/\/isa-afp.org\/entries\/JinjaThreads.html Formal proof development."},{"key":"e_1_3_2_1_32_1","unstructured":"Andreas Lochbihler. 2008. Type Safe Nondeterminism-A Formal Semantics of Java Threads. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2008 ). htp:\/\/www.infsec.ethz.ch\/ people\/andreloc\/publications\/lochbihler08fool.pdf  Andreas Lochbihler. 2008. Type Safe Nondeterminism-A Formal Semantics of Java Threads. In International Workshop on Foundations of Object-Oriented Languages (FOOL 2008 ). htp:\/\/www.infsec.ethz.ch\/ people\/andreloc\/publications\/lochbihler08fool.pdf"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_23"},{"volume-title":"Machine-Checked Formalisation. In Programming Languages and Systems (LNCS","author":"Lochbihler Andreas","key":"e_1_3_2_1_34_1"},{"volume-title":"Interactive Theorem Proving (LNCS","author":"Lochbihler Andreas","key":"e_1_3_2_1_35_1"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"volume-title":"Python: The Full Monty. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (Indianapolis, Indiana, USA) ( OOPSLA '13)","year":"2013","author":"Politz Joe Gibbs","key":"e_1_3_2_1_37_1"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Silvain Rideau and Xavier Leroy. 2010. Validating Register Allocation and Spilling. 224-243. htps:\/\/doi.org\/10.1007\/978-3-642-11970-5_13  Silvain Rideau and Xavier Leroy. 2010. Validating Register Allocation and Spilling. 224-243. htps:\/\/doi.org\/10.1007\/978-3-642-11970-5_13","DOI":"10.1007\/978-3-642-11970-5_13"},{"volume-title":"Asplos","author":"Romer Theodore H","key":"e_1_3_2_1_39_1"},{"volume-title":"Verification, Validation","author":"St\u00e4rk Robert F.","key":"e_1_3_2_1_40_1"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806611"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified validation of lazy code motion. 316-326. htps:\/\/doi.org\/10.1145\/1542476.1542512  Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified validation of lazy code motion. 316-326. htps:\/\/doi.org\/10.1145\/1542476.1542512","DOI":"10.1145\/1543135.1542512"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706311"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544137.2544153"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_3_2_1_47_1","unstructured":"Conrad Watt. 2018. WebAssembly. Archive of Formal Proofs (April 2018 ). htps:\/\/isa-afp.org\/entries\/WebAssembly.html Formal proof development.  Conrad Watt. 2018. WebAssembly. Archive of Formal Proofs (April 2018 ). htps:\/\/isa-afp.org\/entries\/WebAssembly.html Formal proof development."},{"key":"e_1_3_2_1_48_1","first-page":"662","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) ( PLDI 2017 ). Association for Computing Machinery","author":"W\u00fcrthinger Thomas","year":"2017"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509581"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384577.2384587"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2012. Finding and understanding bugs in C compilers. ACM SIGPLAN Notices 47 6 ( 2012 ) 283. htps:\/\/doi.org\/10.1145\/2345156.1993532  Xuejun Yang Yang Chen Eric Eide and John Regehr. 2012. Finding and understanding bugs in C compilers. ACM SIGPLAN Notices 47 6 ( 2012 ) 283. htps:\/\/doi.org\/10.1145\/2345156.1993532","DOI":"10.1145\/2345156.1993532"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Denmark","acronym":"CPP '21"},"container-title":["Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439923","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437992.3439923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:18Z","timestamp":1750193238000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3437992.3439923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,17]]},"references-count":51,"alternative-id":["10.1145\/3437992.3439923","10.1145\/3437992"],"URL":"https:\/\/doi.org\/10.1145\/3437992.3439923","relation":{},"subject":[],"published":{"date-parts":[[2021,1,17]]},"assertion":[{"value":"2021-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}