Login / Signup
CPP
2011
2015
2019
2024
2011
2024
Keyphrases
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
Christina Kohl
,
Aart Middeldorp
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems.
CPP
(2023)
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023
CPP
(2023)
Thomas Lamiaux
,
Axel Ljungström
,
Anders Mörtberg
Computing Cohomology Rings in Cubical Agda.
CPP
(2023)
Floris van Doorn
,
Patrick Massot
,
Oliver Nash
Formalising the h-Principle and Sphere Eversion.
CPP
(2023)
Haobin Ni
,
Antoine Delignat-Lavaud
,
Cédric Fournet
,
Tahina Ramananandro
,
Nikhil Swamy
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER.
CPP
(2023)
Bhavik Mehta
Formalising Sharkovsky's Theorem (Proof Pearl).
CPP
(2023)
Katherine Kosaian
,
Yong Kiam Tan
,
André Platzer
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.
CPP
(2023)
Yannick Forster
,
Felix Jahn
,
Gert Smolka
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl).
CPP
(2023)
Sandrine Blazy
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote).
CPP
(2023)
Anne Baanen
,
Alex J. Best
,
Nirvana Coppola
,
Sander R. Dahmen
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves.
CPP
(2023)
Cezary Kaliszyk
Improved Assistance for Interactive Proof (Keynote).
CPP
(2023)
Kexing Ying
,
Rémy Degenne
A Formalization of Doob's Martingale Convergence Theorems in mathlib.
CPP
(2023)
Yann Herklotz
,
Delphine Demange
,
Sandrine Blazy
Mechanised Semantics for Gated Static Single Assignment.
CPP
(2023)
Hugo Férée
,
Sam van Gool
Formalizing and Computing Propositional Quantifiers.
CPP
(2023)
Jannis Limperg
,
Asta Halkjær From
Aesop: White-Box Best-First Proof Search for Lean.
CPP
(2023)
Eske Hoy Nielsen
,
Danil Annenkov
,
Bas Spitters
Formalising Decentralised Exchanges in Coq.
CPP
(2023)
Xavier Allamigeon
,
Quentin Canu
,
Pierre-Yves Strub
A Formal Disproof of Hirsch Conjecture.
CPP
(2023)
Reynald Affeldt
,
Cyril Cohen
,
Ayumu Saito
Semantics of Probabilistic Programs using s-Finite Kernels in Coq.
CPP
(2023)
Arvind Arasu
,
Tahina Ramananandro
,
Aseem Rastogi
,
Nikhil Swamy
,
Aymeric Fromherz
,
Kesha Hietala
,
Bryan Parno
,
Ravi Ramamurthy
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores.
CPP
(2023)
Brae J. Webb
,
Ian J. Hayes
,
Mark Utting
Verifying Term Graph Optimizations using Isabelle/HOL.
CPP
(2023)
Anthony Bordg
,
Adrián Doña Mateo
Encoding Dependently-Typed Constructions into Simple Type Theory.
CPP
(2023)
Matthew L. Daggitt
,
Robert Atkey
,
Wen Kokke
,
Ekaterina Komendantskaya
,
Luca Arnaboldi
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively.
CPP
(2023)
Joshua Clune
A Formalized Reduction of Keller's Conjecture.
CPP
(2023)
Michael Färber
Terms for Efficient Proof Checking and Parsing.
CPP
(2023)
Angeliki Koutsoukou-Argyraki
,
Mantas Baksys
,
Chelsea Edmonds
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL.
CPP
(2023)
Benjamin Grégoire
,
Jean-Christophe Léchenet
,
Enrico Tassi
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.
CPP
(2023)
Valentin Blot
,
Denis Cousineau
,
Enzo Crance
,
Louise Dubois de Prisque
,
Chantal Keller
,
Assia Mahboubi
,
Pierre Vial
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory.
CPP
(2023)
Rudy Peterson
,
Eric Hayden Campbell
,
John Chen
,
Natalie Isak
,
Calvin Shyu
,
Ryan Doenges
,
Parisa Ataei
,
Nate Foster
P4Cub: A Little Language for Big Routers.
CPP
(2023)