| 2015 | A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. | Fabian Immler |
| 2015 | Premise Selection and External Provers for HOL4. | Thibault Gauthier, Cezary Kaliszyk |
| 2015 | Certified Normalization of Context-Free Grammars. | Denis Firsov, Tarmo Uustalu |
| 2015 | A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. | Manuel Eberl |
| 2015 | A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller |
| 2015 | Practical Tactics for Verifying C Programs in Coq. | Jingyuan Cao, Ming Fu, Xinyu Feng |
| 2015 | Certified Abstract Interpretation with Pretty-Big-Step Semantics. | Martin Bodin, Thomas P. Jensen, Alan Schmitt |
| 2015 | Verified Validation of Program Slicing. | Sandrine Blazy, Andr Maroneze, David Pichardie |
| 2015 | Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. | Yves Bertot |
| 2015 | The Speedup Theorem in a Primitive Recursive Framework. | Andrea Asperti |
| 2013 | A Formal Model and Correctness Proof for an Access Control Policy Framework. | Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2013 | Computational Verification of Network Programs in Coq. | Gordon Stewart |
| 2013 | Certified Kruskal's Tree Theorem. | Christian Sternagel |
| 2013 | Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. | Andreas Schropp, Andrei Popescu |
| 2013 | Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. | Magnus O. Myreen, Gregorio Curello |
| 2013 | Extracting Proofs from Tabled Proof Search. | Dale Miller, Alwen Tiu |
| 2013 | π n (S n ) in Homotopy Type Theory. | Daniel R. Licata, Guillaume Brunerie |
| 2013 | Aliasing Restrictions of C11 Formalized in Coq. | Robbert Krebbers |
| 2013 | Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. | Narges Khakpour, Oliver Schwarz, Mads Dam |
| 2013 | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. | Brian Huffman, Ondrej Kuncar |
| 2013 | Formalizing the SAFECode Type System. | Daniel Huang, Greg Morrisett |
| 2013 | Certified Parsing of Regular Languages. | Denis Firsov, Tarmo Uustalu |
| 2013 | Mostly Sound Type System Improves a Foundational Program Verifier. | Josiah Dodds, Andrew W. Appel |
| 2013 | A Constructive Theory of Regular Languages in Coq. | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
| 2013 | Refinements for Free! | Cyril Cohen, Maxime Dns, Anders Mrtberg |