| 2013 | Certifiably Sound Parallelizing Transformations. | Christian J. Bell |
| 2013 | Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. | Olivier Savary Blanger, Stefan Monnier, Brigitte Pientka |
| 2013 | A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem. | Andrea Asperti |
| 2013 | Formalizing Probabilistic Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2012 | Mechanized Verification of Computing Dominators for Formalizing Compilers. | Jianzhou Zhao, Steve Zdancewic |
| 2012 | Compositional Verification of a Baby Virtual Memory Manager. | Alexander Vaynberg, Zhong Shao |
| 2012 | Producing Certified Functional Code from Inductive Specifications. | Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois |
| 2012 | A Formally-Verified Alias Analysis. | Valentin Robert, Xavier Leroy |
| 2012 | Proving Concurrent Noninterference. | Andrei Popescu, Johannes Hlzl, Tobias Nipkow |
| 2012 | A Formal Proof of Square Root and Division Elimination in Embedded Programs. | Pierre Neron |
| 2012 | Shall We Juggle, Coinductively? | Keisuke Nakano |
| 2012 | Noninterference for Operating System Kernels. | Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein |
| 2012 | On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. | Dominic P. Mulligan, Claudio Sacerdoti Coen |
| 2012 | Scalable Formal Machine Models. | Greg Morrisett |
| 2012 | Mechanized Semantics for Compiler Verification. | Xavier Leroy |
| 2012 | Program Certification by Higher-Order Model Checking. | Naoki Kobayashi |
| 2012 | Constructive Completeness for Modal Logic with Transitive Closure. | Christian Doczkal, Gert Smolka |
| 2012 | Coherent and Strongly Discrete Rings in Type Theory. | Thierry Coquand, Anders Mrtberg, Vincent Siles |
| 2012 | Compact Proof Certificates for Linear Logic. | Kaustuv Chaudhuri |
| 2012 | A String of Pearls: Proofs of Fermat's Little Theorem. | Hing-Lun Chan, Michael Norrish |
| 2012 | An Executable Semantics for CompCert C. | Brian Campbell |
| 2012 | The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. | Lukas Bulwahn |
| 2012 | Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. | Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
| 2012 | Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Santiago Zanella-Bguelin |
| 2012 | Rating Disambiguation Errors. | Andrea Asperti, Wilmer Ricciotti |