"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.
"Generating Good Generators for Inductive Relations", POPL 2018, Leonidas Lampropoulos, Zoe Paraskevopoulou, Benjamin C. Pierce.
"Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac", ITP 2018, Jason Gross, Andres Erbsen, Adam Chlipala.
"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.
"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.
"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.