Abstract is missing.
- Under-Approximation for Scalable Bug Detection (Keynote)Azalea Raad. 1 [doi]
- UTC Time, Formally VerifiedAna de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten. 2-13 [doi]
- VCFloat2: Floating-Point Error Analysis in CoqAndrew W. Appel, Ariel Kellison. 14-29 [doi]
- The Last Yard: Foundational End-to-End Verification of High-Speed CryptographyPhilipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters. 30-44 [doi]
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation LogicQiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur 0001, Ilya Sergey. 45-59 [doi]
- Compositional Verification of Concurrent C Programs with Search Structure TemplatesDuc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang. 60-74 [doi]
- Unification for Subformula Linking under QuantifiersIke Mulder, Robbert Krebbers. 75-88 [doi]
- PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision DiagramsClément Chavanon, Frédéric Besson, Tristan Ninet. 89-102 [doi]
- Memory Simulations, Security and Optimization in a Verified CompilerDavid Monniaux. 103-117 [doi]
- Lean Formalization of Extended Regular Expression Matching with LookaroundsEkaterina Zhuchko, Margus Veanes, Gabriel Ebner. 118-131 [doi]
- Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local LemmaChelsea Edmonds, Lawrence C. Paulson. 132-146 [doi]
- Certification of Confluence- and Commutation-Proofs via Parallel Critical PairsNao Hirokawa, Dohan Kim 0001, Kiraku Shintani, René Thiemann. 147-161 [doi]
- A Temporal Differential Dynamic Logic Formal EmbeddingLauren White, Laura Titolo, J. Tanner Slagel, César A. Muñoz. 162-176 [doi]
- Formalizing Giles Gardam's Disproof of Kaplansky's Unit ConjectureSiddhartha Gadgil, Anand Rao Tadipatri. 177-189 [doi]
- A Formalization of Complete Discrete Valuation Rings and Local FieldsMaría Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio. 190-204 [doi]
- Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple ArgumentsJoseph Eremondi. 205-217 [doi]
- A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic LogicIan Shillito, Dominik Kirst. 218-229 [doi]
- Martin-Löf à la CoqArthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet. 230-245 [doi]
- Univalent Double CategoriesNiels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North. 246-259 [doi]
- Displayed Monoidal Categories for the Semantics of Linear LogicBenedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert. 260-273 [doi]
- Formalizing the ∞-Categorical Yoneda LemmaNikolai Kudasov, Emily Riehl, Jonathan Weinberger. 274-290 [doi]