CPP

Publications

2024

Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang
Compositional Verification of Concurrent C Programs with Search Structure Templates. CPP (2024)
David Monniaux
Memory Simulations, Security and Optimization in a Verified Compiler. CPP (2024)
Ian Shillito, Dominik Kirst
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. CPP (2024)
Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten
UTC Time, Formally Verified. CPP (2024)
Ike Mulder, Robbert Krebbers
Unification for Subformula Linking under Quantifiers. CPP (2024)
Joseph Eremondi
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. CPP (2024)
Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. CPP (2024)
Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner
Lean Formalization of Extended Regular Expression Matching with Lookarounds. CPP (2024)
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 CPP (2024)
Chelsea Edmonds, Lawrence C. Paulson
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. CPP (2024)
Nikolai Kudasov, Emily Riehl, Jonathan Weinberger
Formalizing the ∞-Categorical Yoneda Lemma. CPP (2024)
Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert
Displayed Monoidal Categories for the Semantics of Linear Logic. CPP (2024)
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. CPP (2024)
Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North
Univalent Double Categories. CPP (2024)
Andrew W. Appel, Ariel Kellison
VCFloat2: Floating-Point Error Analysis in Coq. CPP (2024)
María Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio
A Formalization of Complete Discrete Valuation Rings and Local Fields. CPP (2024)
Siddhartha Gadgil, Anand Rao Tadipatri
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. CPP (2024)
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet
Martin-Löf à la Coq. CPP (2024)
Lauren White, Laura Titolo, J. Tanner Slagel, César A. Muñoz
A Temporal Differential Dynamic Logic Formal Embedding. CPP (2024)
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. CPP (2024)
Clément Chavanon, Frédéric Besson, Tristan Ninet
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. CPP (2024)
Azalea Raad
Under-Approximation for Scalable Bug Detection (Keynote). CPP (2024)

2023