| 2016 | Formalising Semantics for Expected Running Time of Probabilistic Programs. | Johannes Hlzl |
| 2016 | Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms. | Thomas Grgoire, Adam Chlipala |
| 2016 | Two-Way Automata in Coq. | Christian Doczkal, Gert Smolka |
| 2016 | Proof Pearl: Bounding Least Common Multiples with Triangles. | Hing-Lun Chan, Michael Norrish |
| 2016 | Cardinalities of Finite Relations in Coq. | Paul Brunet, Damien Pous, Insa Stucke |
| 2016 | Visual Theorem Proving with the Incredible Proof Machine. | Joachim Breitner |
| 2016 | Mechanical Verification of a Constructive Proof for FLP. | Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann |
| 2016 | CoSMed: A Confidentiality-Verified Social Media Platform. | Thomas Bauerei, Armando Pesenti Gritti, Andrei Popescu, Franco Raimondi |
| 2016 | POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). | Fahad Ausaf, Roy Dyckhoff, Christian Urban |
| 2016 | Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. | June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah |
| 2016 | Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of Paths. | Romain Assat, Frdric Voisin, Burkhart Wolff |
| 2016 | HOL Zero's Solutions for Pollack-Inconsistency. | Mark Adams |
| 2016 | An Isabelle/HOL Formalisation of Green's Theorem. | Mohammad Abdulaziz, Lawrence C. Paulson |
| 2016 | What's in a Theorem Name? | David Aspinall, Cezary Kaliszyk |
| 2015 | Pattern Matches in HOL: - A New Representation and Improved Code Generation. | Thomas Tuerk, Magnus O. Myreen, Ramana Kumar |
| 2015 | Deriving Comparators and Show Functions in Isabelle/HOL. | Christian Sternagel, Ren Thiemann |
| 2015 | A Mechanized Theory of Regular Trees in Dependent Type Theory. | Rgis Spadotti |
| 2015 | Transfinite Constructions in Classical Type Theory. | Gert Smolka, Steven Schfer, Christian Doczkal |
| 2015 | ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. | Filip Sieczkowski, Ales Bizjak, Lars Birkedal |
| 2015 | A Linear First-Order Functional Intermediate Language for Verified Compilers. | Sigurd Schneider, Gert Smolka, Sebastian Hack |
| 2015 | Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. | Steven Schfer, Tobias Tebbi, Gert Smolka |
| 2015 | Formalising Knot Theory in Isabelle/HOL. | T. V. H. Prathamesh |
| 2015 | Foundational Property-Based Testing. | Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dns, Leonidas Lampropoulos, Benjamin C. Pierce |
| 2015 | Amortized Complexity Verified. | Tobias Nipkow |
| 2015 | Affine Arithmetic and Applications to Real-Number Proving. | Mariano M. Moscato, Csar A. Muoz, Andrew P. Smith |