| 2012 | A Formal Proof of Square Root and Division Elimination in Embedded Programs. Pierre Neron |
| 2012 | A Formally-Verified Alias Analysis. Valentin Robert, Xavier Leroy |
| 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 | Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin |
| 2012 | Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings Chris Hawblitzel, Dale Miller |
| 2012 | Coherent and Strongly Discrete Rings in Type Theory. Thierry Coquand, Anders Mörtberg, Vincent Siles |
| 2012 | Compact Proof Certificates for Linear Logic. Kaustuv Chaudhuri |
| 2012 | Compositional Verification of a Baby Virtual Memory Manager. Alexander Vaynberg, Zhong Shao |
| 2012 | Constructive Completeness for Modal Logic with Transitive Closure. Christian Doczkal, Gert Smolka |
| 2012 | Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. Sylvie Boldo, Catherine Lelay, Guillaume Melquiond |
| 2012 | Mechanized Semantics for Compiler Verification. Xavier Leroy |
| 2012 | Mechanized Verification of Computing Dominators for Formalizing Compilers. Jianzhou Zhao, Steve Zdancewic |
| 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 | Producing Certified Functional Code from Inductive Specifications. Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois |
| 2012 | Program Certification by Higher-Order Model Checking. Naoki Kobayashi |
| 2012 | Proof Pearl: Abella Formalization of λ-Calculus Cube Property. Beniamino Accattoli |
| 2012 | Proving Concurrent Noninterference. Andrei Popescu, Johannes Hölzl, Tobias Nipkow |
| 2012 | Rating Disambiguation Errors. Andrea Asperti, Wilmer Ricciotti |
| 2012 | Scalable Formal Machine Models. Greg Morrisett |
| 2012 | Shall We Juggle, Coinductively? Keisuke Nakano |
| 2012 | The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. Lukas Bulwahn |