| 2015 | A Compositional Semantics for Verified Separate Compilation and Linking. Tahina Ramananandro, Zhong Shao, Shu-Chun Weng, Jérémie Koenig, Yuchen Fu |
| 2015 | A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. Manuel Eberl |
| 2015 | A Framework for Verifying Depth-First Search Algorithms. Peter Lammich, René Neumann |
| 2015 | A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. Kaustuv Chaudhuri, Matteo Cimini, Dale Miller |
| 2015 | A Typed C11 Semantics for Interactive Theorem Proving. Robbert Krebbers, Freek Wiedijk |
| 2015 | A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection. Fabian Immler |
| 2015 | Certified Abstract Interpretation with Pretty-Big-Step Semantics. Martin Bodin, Thomas P. Jensen, Alan Schmitt |
| 2015 | Certified Connection Tableaux Proofs for HOL Light and TPTP. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil |
| 2015 | Certified Normalization of Context-Free Grammars. Denis Firsov, Tarmo Uustalu |
| 2015 | Clean-Slate Development of Certified OS Kernels. Zhong Shao |
| 2015 | Completeness and Decidability of de Bruijn Substitution Algebra in Coq. Steven Schäfer, Gert Smolka, Tobias Tebbi |
| 2015 | Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants. Ondrej Kuncar |
| 2015 | Fixed Precision Patterns for the Formal Verification of Mathematical Constant Approximations. Yves Bertot |
| 2015 | Formal Reasoning about the C11 Weak Memory Model. Viktor Vafeiadis |
| 2015 | Practical Tactics for Verifying C Programs in Coq. Jingyuan Cao, Ming Fu, Xinyu Feng |
| 2015 | Premise Selection and External Provers for HOL4. Thibault Gauthier, Cezary Kaliszyk |
| 2015 | Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015 Xavier Leroy, Alwen Tiu |
| 2015 | Proving Lock-Freedom Easily and Automatically. Xiao Jia, Wei Li, Viktor Vafeiadis |
| 2015 | Recording Completion for Certificates in Equational Reasoning. Thomas Sternagel, Sarah Winkler, Harald Zankl |
| 2015 | The Speedup Theorem in a Primitive Recursive Framework. Andrea Asperti |
| 2015 | Verified Validation of Program Slicing. Sandrine Blazy, André Maroneze, David Pichardie |