| 2013 | Towards Certifying Network Calculus. | Etienne Mabille, Marc Boyer, Loc Fejoz, Stephan Merz |
| 2013 | Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. | Andreas Lochbihler |
| 2013 | Formal Reasoning about Classified Markov Chains in HOL. | Liya Liu, Osman Hasan, Vincent Aravantinos, Sofine Tahar |
| 2013 | Automating Theorem Proving with SMT. | K. Rustan M. Leino |
| 2013 | Automatic Data Refinement. | Peter Lammich |
| 2013 | MaSh: Machine Learning for Sledgehammer. | Daniel Khlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban |
| 2013 | Scalable LCF-Style Proof Translation. | Cezary Kaliszyk, Alexander Krauss |
| 2013 | Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. | Johannes Hlzl, Fabian Immler, Brian Huffman |
| 2013 | Data Refinement in Isabelle/HOL. | Florian Haftmann, Alexander Krauss, Ondrej Kuncar, Tobias Nipkow |
| 2013 | A Machine-Checked Proof of the Odd Order Theorem. | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Franois Garillot, Stphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Thry |
| 2013 | Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. | Jrg Endrullis, Dimitri Hendriks, Martin Bodin |
| 2013 | Pragmatic Quotient Types in Coq. | Cyril Cohen |
| 2013 | Practical Probability: Applying pGCL to Lattice Scheduling. | David A. Cock |
| 2013 | Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. | Guillaume Claret, Lourdes Del Carmen Gonzlez-Huesca, Yann Rgis-Gianas, Beta Ziliani |
| 2013 | Subformula Linking as an Interaction Method. | Kaustuv Chaudhuri |
| 2013 | Implementing Hash-Consed Structures in Coq. | Thomas Braibant, Jacques-Henri Jourdan, David Monniaux |
| 2013 | Applying Formal Methods in the Large. | Dominique Bolignano |
| 2013 | Stateless Higher-Order Logic with Quantified Types. | Evan Austin, Perry Alexander |
| 2013 | Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. | Alasdair Armstrong, Georg Struth, Tjark Weber |
| 2012 | Priority Inheritance Protocol Proved Correct. | Xingyuan Zhang, Christian Urban, Chunhan Wu |
| 2012 | Stop When You Are Almost-Full - Adventures in Constructive Termination. | Dimitrios Vytiniotis, Thierry Coquand, David Wahlstedt |
| 2012 | Certification of Nontermination Proofs. | Christian Sternagel, Ren Thiemann |
| 2012 | A Differential Operator Approach to Equational Differential Invariants - (Invited Paper). | Andr Platzer |
| 2012 | MetiTarski: Past and Future. | Lawrence C. Paulson |
| 2012 | Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem. | Lars Noschinski |