| 2012 | Abstract Interpretation of Annotated Commands. | Tobias Nipkow |
| 2012 | Functional Programs: Conversions between Deep and Shallow Embeddings. | Magnus O. Myreen |
| 2012 | Synthesis of Distributed Mobile Programs Using Monadic Types in Coq. | Marino Miculan, Marco Paviotti |
| 2012 | Verifying and Generating WP Transformers for Procedures on Complex Data. | Patrick Michel, Arnd Poetzsch-Heffter |
| 2012 | Using Locales to Define a Rely-Guarantee Temporal Logic. | William Mansky, Elsa L. Gunter |
| 2012 | Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm. | Peter Lammich, Thomas Tuerk |
| 2012 | Standalone Tactics Using OpenTheory. | Ramana Kumar, Joe Hurd |
| 2012 | Mechanised Separation Algebra. | Gerwin Klein, Rafal Kolanski, Andrew Boyton |
| 2012 | Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. | Fabian Immler, Johannes Hlzl |
| 2012 | Bridging the Gap: Automatic Verified Abstraction of C. | David Greenaway, June Andronick, Gerwin Klein |
| 2012 | A Language of Patterns for Subterm Selection. | Georges Gonthier, Enrico Tassi |
| 2012 | A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. | Ruben Gamboa, John R. Cowles |
| 2012 | Abella: A Tutorial. | Andrew Gacek |
| 2012 | Directions in ISA Specification. | Anthony C. J. Fox |
| 2012 | A Refinement-Based Approach to Computational Algebra in Coq. | Maxime Dns, Anders Mrtberg, Vincent Siles |
| 2012 | Bag Equivalence via a Proof-Relevant Membership Relation. | Nils Anders Danielsson |
| 2012 | Construction of Real Algebraic Numbers in Coq. | Cyril Cohen |
| 2012 | More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification. | Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach |
| 2012 | Charge! - A Framework for Higher-Order Separation Logic in Coq. | Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal |
| 2012 | Computer-Aided Cryptographic Proofs. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Santiago Zanella-Bguelin |
| 2012 | Towards Provably Robust Watermarking. | David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring |
| 2012 | A Compact Proof of Decidability for Regular Expression Equivalence. | Andrea Asperti |
| 2012 | Formalization of Shannon's Theorems in SSReflect-Coq. | Reynald Affeldt, Manabu Hagiwara |
| 2011 | A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). | Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2011 | WorkingWiki: a MediaWiki-based platform for collaborative research. | Lee Worden |