| 2025 | A CHERI C Memory Model for Verified Temporal Safety. Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell |
| 2025 | An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting. Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada |
| 2025 | An Isabelle/HOL Framework for Synthetic Completeness Proofs. Asta Halkjær From |
| 2025 | CRIS: The Power of Imagination in Specification and Verification (Invited Talk). Chung-Kil Hur |
| 2025 | CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq. Wolfgang Meier, Martin Jensen, Jean Pichon-Pharabod, Bas Spitters |
| 2025 | Certifying Rings of Integers in Number Fields. Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen |
| 2025 | Formalization of Differential Privacy in Isabelle/HOL. Tetsuya Sato, Yasuhiko Minamide |
| 2025 | Formalized Burrows-Wheeler Transform. Louis Cheung, Alistair Moffat, Christine Rizkallah |
| 2025 | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. Christina Kirk, Aart Middeldorp |
| 2025 | Formalizing the One-Way to Hiding Theorem. Katharina Heidler, Dominique Unruh |
| 2025 | Formally Verified Hardening of C Programs against Hardware Fault Injection. Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet |
| 2025 | Further Tackling Post Correspondence Problem and Proof Generation. Akihiro Omori, Yasuhiko Minamide |
| 2025 | Intrinsically Correct Sorting in Cubical Agda. Cass Alexandru, Vikraman Choudhury, Jurriaan Rot, Niels van der Weide |
| 2025 | Leakage-Free Probabilistic Jasmin Programs. José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh |
| 2025 | Machine Checked Proofs and Programs in Algebraic Combinatorics. Florent Hivert |
| 2025 | Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR. Nicolas Chappe, Ludovic Henrio, Yannick Zakowski |
| 2025 | Nominal Matching Logic with Fixpoints. Mircea Sebe, Maribel Fernández, James Cheney |
| 2025 | Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025 Kathrin Stark, Amin Timany, Sandrine Blazy, Nicolas Tabareau |
| 2025 | Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk). Emily Riehl |
| 2025 | Split Decisions: Explicit Contexts for Substructural Languages. Daniel Zackon, Chuta Sano, Alberto Momigliano, Brigitte Pientka |
| 2025 | Tactic Script Optimisation for Aesop. Jannis Limperg |
| 2025 | The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. Simon Friis Vindum, Aïna Linn Georges, Lars Birkedal |
| 2025 | Verified and Efficient Matching of Regular Expressions with Lookaround. Agnishom Chattopadhyay, Angela W. Li, Konstantinos Mamouras |