DeepSpec
 
The Science of Deep Specification
"A Specification for Dependently-Typed Haskell", Submitted for publication 2017, Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, Richard Eisenberg.
"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.
"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.
"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 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.