| 2024 | Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. | Qiyuan Zhao, George Prlea, Zhendong Ang, Umang Mathur, Ilya Sergey |
| 2024 | A Temporal Differential Dynamic Logic Formal Embedding. | Lauren M. White, Laura Titolo, J. Tanner Slagel, Csar A. Muoz |
| 2024 | Univalent Double Categories. | Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North |
| 2024 | A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. | Ian Shillito, Dominik Kirst |
| 2024 | Under-Approximation for Scalable Bug Detection (Keynote). | Azalea Raad |
| 2024 | Compositional Verification of Concurrent C Programs with Search Structure Templates. | Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang |
| 2024 | Unification for Subformula Linking under Quantifiers. | Ike Mulder, Robbert Krebbers |
| 2024 | Memory Simulations, Security and Optimization in a Verified Compiler. | David Monniaux |
| 2024 | Formalizing the ∞-Categorical Yoneda Lemma. | Nikolai Kudasov, Emily Riehl, Jonathan Weinberger |
| 2024 | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. | Nao Hirokawa, Dohan Kim, Kiraku Shintani, Ren Thiemann |
| 2024 | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. | Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Tho Winterhalter, Catalin Hritcu, Bas Spitters |
| 2024 | Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. | Siddhartha Gadgil, Anand Rao Tadipatri |
| 2024 | A Formalization of Complete Discrete Valuation Rings and Local Fields. | Mara Ins de Frutos-Fernndez, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio |
| 2024 | Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. | Joseph Eremondi |
| 2024 | Formal Probabilistic Methods for Combinatorial Structures using the Lovsz Local Lemma. | Chelsea Edmonds, Lawrence C. Paulson |
| 2024 | PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. | Clment Chavanon, Frdric Besson, Tristan Ninet |
| 2024 | UTC Time, Formally Verified. | Ana de Almeida Borges, Mireia Gonzlez Bedmar, Juan Jos Conejero Rodrguez, Eduardo Hermo Reyes, Joaquim Casals Buuel, Joost J. Joosten |
| 2024 | VCFloat2: Floating-Point Error Analysis in Coq. | Andrew W. Appel, Ariel Kellison |
| 2024 | Displayed Monoidal Categories for the Semantics of Linear Logic. | Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert |
| 2024 | Martin-Lf la Coq. | Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pdrot, Loc Pujet |
| 2023 | A Formalization of Doob's Martingale Convergence Theorems in mathlib. | Kexing Ying, Rmy Degenne |
| 2023 | Verifying Term Graph Optimizations using Isabelle/HOL. | Brae J. Webb, Ian J. Hayes, Mark Utting |
| 2023 | P4Cub: A Little Language for Big Routers. | Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster |
| 2023 | Formalising Decentralised Exchanges in Coq. | Eske Hoy Nielsen, Danil Annenkov, Bas Spitters |
| 2023 | ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. | Haobin Ni, Antoine Delignat-Lavaud, Cdric Fournet, Tahina Ramananandro, Nikhil Swamy |