CompCert(C)

1. POPL

   Formal certification of a compiler back-end or: programming a compiler with a proof assistant Leroy, Xavier In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006 2006
2. JAR

   Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations Leroy, Xavier, and Blazy, Sandrine J. Autom. Reason. 2008
3. CACM

   Formal verification of a realistic compiler Leroy, Xavier Commun. ACM 2009
4. JAR

   Mechanized Semantics for the Clight Subset of the C Language Blazy, Sandrine, and Leroy, Xavier J. Autom. Reason. 2009
5. PLDI

   Towards certified separate compilation for concurrent programs Jiang, Hanru, Liang, Hongjin, Xiao, Siyang, Zha, Junpeng, and Feng, Xinyu In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019 2019

AutoCorres(C)

1. POPL

   Types, bytes, and separation logic Tuch, Harvey, Klein, Gerwin, and Norrish, Michael In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007 2007
2. ITP

   Bridging the Gap: Automatic Verified Abstraction of C Greenaway, David, Andronick, June, and Klein, Gerwin In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 2012
3. PLDI

   Don’t sweat the small stuff: formal verification of C code without the pain Greenaway, David, Lim, Japheth, Andronick, June, and Klein, Gerwin In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014 2014

JAVA

1. ESOP

   Verifying a Compiler for Java Threads Lochbihler, Andreas In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings 2010
2. ESOP

   Java and the Java Memory Model - A Unified, Machine-Checked Formalisation Lochbihler, Andreas In Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings 2012
3. TOPLAS

   Making the java memory model safe Lochbihler, Andreas ACM Trans. Program. Lang. Syst. 2013

LLVM

1. POPL

   Formalizing the LLVM intermediate representation for verified program transformations Zhao, Jianzhou, Nagarakatte, Santosh, Martin, Milo M. K., and Zdancewic, Steve In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012 2012
2. ITP

   Generating Verified LLVM from Isabelle/HOL Lammich, Peter In 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA 2019

CakeML

1. ICFP

   A new verified compiler backend for CakeML Tan, Yong Kiam, Myreen, Magnus O., Kumar, Ramana, Fox, Anthony C. J., Owens, Scott, and Norrish, Michael In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016 2016
2. ESOP

   A Verified Compiler from Isabelle/HOL to CakeML Hupel, Lars, and Nipkow, Tobias In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 2018
3. JAR

   A Verified Generational Garbage Collector for CakeML Ericsson, Adam Sandberg, Myreen, Magnus O., and Pohjola, Johannes J. Autom. Reason. 2019
4. The verified CakeML compiler backend Tan, Yong Kiam, Myreen, Magnus O., Kumar, Ramana, Fox, Anthony C. J., Owens, Scott, and Norrish, Michael J. Funct. Program. 2019

Rust

1. POPL

   RustBelt: securing the foundations of the rust programming language Jung, Ralf, Jourdan, Jacques-Henri, Krebbers, Robbert, and Dreyer, Derek Proc. ACM Program. Lang. 2018
2. TASE

   KRust: A Formal Executable Semantics of Rust Wang, Feng, Song, Fu, Zhang, Min, Zhu, Xiaoran, and Zhang, Jun In 2018 International Symposium on Theoretical Aspects of Software Engineering, TASE 2018, Guangzhou, China, August 29-31, 2018 2018

Lustre

1. PLDI

   A formally verified compiler for Lustre Bourke, Timothy, Brun, Lélio, Dagand, Pierre-Évariste, Leroy, Xavier, Pouzet, Marc, and Rieg, Lionel In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017 2017
2. POPL

   Mechanized semantics and verified compilation for a dataflow synchronous language with reset Bourke, Timothy, Brun, Lélio, and Pouzet, Marc Proc. ACM Program. Lang. 2020