"An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code", POPL 2019, Pierre Wilke, Yuting Wang, Zhong Shao.
"From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server", CPP 2019, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C. Pierce, Steve Zdancewic.
"Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises", IEEE Security & Privacy 2019, Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala.
"A Promise Checked Is a Promise Kept: Inspection Testing", Haskell Symposium 2018, Joachim Breitner.
"Certified Concurrent Abstraction Layers", PLDI 2018, Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, Tahina Ramananandro.
"Generating Good Generators for Inductive Relations", POPL 2018, Leonidas Lampropoulos, Zoe Paraskevopoulou, Benjamin C. Pierce.
"Keep Your Laziness in Check", Proceedings of the ACM on Programming Languages archive Volume 2 Issue ICFP, September 2018 Article No. 102 2018, Kenneth Foner, Hengchu Zhang, Leonidas Lampropoulos.
"Ready, set, verify! Applying hs-to-coq to real-world Haskell code (experience report)", Proceedings of the ACM on Programming Languages. Volume 2 Issue ICFP, September 2018 2018, Antal Spector-Zabusky, Christine Rizkallah, Joachim Breitner, John Wiegley, Stephanie Weirich, Yao Li.
"Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac", ITP 2018, Jason Gross, Andres Erbsen, Adam Chlipala.
"Schematic Polymorphism in the Abella Proof Assistant", Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP) 2018, Gopalan Nadathur, Yuting Wang.
"Total Haskell is Reasonable Coq", Proceedings of 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'18) 2018, Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich.
"Toward Compositional Verification of Interruptible OS Kernels and Device Drivers (Extended Version)", Journal of Automated Reasoning (JAR) 2018, Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu.
"VST-Floyd: A separation logic tool to verify correctness of C programs", Journal of Automated Reasoning 2018, Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel.
"What's the Difference? A Functional Pearl on Subtracting Bijections", Proc. ACM Program. Lang. 2, ICFP, Article 101 2018, Kenneth Foner.
"A Formal Equational Theory for Call-By-Push-Value", 9th International Conference on Interactive Theorem Proving (ITP) 2017, Christine Rizkallah, Dmitri Garbuzov, Steve Zdancewic.
"A Specification for Dependent-Types in Haskell", ICFP 2017, 22nd ACM SIGPLAN International Conference on Functional Programming 2017, Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, Richard Eisenberg.
"A verified messaging system", OOPSLA 2017, William Mansky, Aleksey Nogin, Andrew W. Appel.
"Automated Resource Analysis with Coq Proof Objects", CAV 2017: 29th International Conference on Computer Aided Verification 2017, Quentin Carbonneaux, Jan Hoffmann, Thomas Reps, Zhong Shao.
"Beginner's Luck: A Language for Random Generators", POPL 2017, Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Li-yao Xia.
"Bringing order to the separation logic jungle", APLAS'17: 15th Asian Symposium on Programming Languages and Systems 2017, Qinxiang Cao, Santiago Cuellar, Andrew W. Appel.
"CertiCoq: A verified compiler for Coq", CoqPL 2017, Abhishek Anand, Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, Matthew Weaver.
"Kami: A Platform for High-Level Parametric Hardware Specification and its Modular Verification", ICFP 2017, Joonwon Choi, Murali Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind.
"Logical Foundations", Volume 1 of Software Foundations 2017, Benjamin C. Pierce.
"Position paper: the science of deep specification", Philosophical Transactions of the Royal Society A 2017, Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, Steve Zdancewic.
"Programming Language Foundations", Volume 2 of Software Foundations 2017, Benjamin C. Pierce.
"Safety and Liveness of MCS Lock---Layer by Layer", APLAS'17: 15th Asian Symposium on Programming Languages and Systems 2017, Jieung Kim, Vilhelm Sjöberg, Ronghui Gu, Zhong Shao.
"Shrink Fast Correctly!", PPDP'17: 19th International Symposium on Principles and Practice of Declarative Programming 2017, Olivier Savary Belanger, Andrew W. Appel.
"Verified Functional Algorithms", Volume 3 of the Software Foundations series 2017, Andrew W. Appel.
"Verified correctness and security of mbedTLS HMAC-DRBG", CCS'17: ACM Conference on Computer and Communication Security 2017, Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, Andrew W. Appel.
"Verifying Dynamic Race Detection", The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017) 2017, William Mansky, Yuanfeng Peng, Steve Zdancewic, Joe Devietti.
"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels", OSDI 2016, Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, David Costanzo.
"End-to-End Verification of Information-Flow Security for C and Assembly Programs", PLDI 2016, David Costanzo, Zhong Shao, Ronghui Gu.
"Modular Verification for Computer Security", CSF'16: Computer Security Foundations Symposium 2016, Andrew W. Appel.
"Toward Compositional Verification of Interruptible OS Kernels and Device Drivers", PLDI 2016, Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu.
"Modular Deductive Verification of Multiprocessor Hardware Designs", CAV 2015, Murali Vijayaraghavan, Adam Chlipala, Arvind, Nirav Dave.
"Formal Verification of Hardware Synthesis", CAV 2013, Thomas Braibant, Adam Chlipala.