CPP 2024
as the organisers put it
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education. CPP is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2024 will be held on 15-16 January 2024 and will be co-located with POPL 2024 in London, UK.
who it's for
formal methods researchers, proof engineers, theorem prover developers, verification engineers, programming language researchers, security engineers, compiler engineers
topics
Incorrectness Separation Logic; bi-abductive interprocedural analysis; Coq cryptography pipeline (Hacspec↔Jasmin↔SSProve); verified UTC conversion with leap seconds; floating-point error bounds in Coq (VCFloat2); differential dynamic logic embedding in PVS; machine-checked Lovász Local Lemma; certified confluence via parallel critical pairs; Lean formalization of local fields; formal counterexample to Kaplansky's unit conjecture; interactive proof automation and ML-guided search; verified compilers and memory-security simulations
| title | author | length |
|---|---|---|
| Under-approximation for Scalable Bug Detection | Azalea Raad | 59m |
Presents a concrete under‑approximate program logic, Incorrectness Separation Logic, and an automated analyzer Pulse‑X that targets memory‑safety bugs (null… | ||
| A mechanised and constructive reverse analysis of soundness and completeness of b... | Ian Shillito, Dominik Kirst | 32m |
A Coq formalisation verifies propositional bi‑intuitionistic soundness and shows soundness forces classicality: soundness implies excluded middle in the… | ||
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography | Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Cătălin Hriţcu, Bas Spitters | 23m |
Coq is used to connect Hacspec, Jasmin and SSProve into an automated pipeline that produces: a functional Hacspec spec, an imperative SSProve spec, and… | ||
| UTC time, formally verified | Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten | 31m |
A verified UTC conversion library implemented in Coq with MathComp that implements leap seconds (27 added since 1972) and proves bidirectional correctness… | ||
| VCFloat2: Floating-point error analysis in Coq | Andrew W. Appel, Ariel E. Kellison | 31m |
VCFloat2 is a Coq tool that automatically and soundly computes floating‑point round‑off error bounds with computational reflection, handling nonstandard… | ||
| A Temporal Differential Dynamic Logic Formal Embedding | Lauren White, Laura Titolo, J Tanner Slagel, Cesar Munoz | 29m |
This work embeds dTL2 embedded in PVS by formalizing a trace semantics, a proof calculus extended for universally quantified reachability, and tactics so… | ||
| Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local ... | Chelsea Edmonds, Lawrence Paulson | 32m |
Presents a reusable Isabelle/HOL framework that formalises probabilistic existence proofs and gives the first machine-checked proof of the Lovász Local Lemma… | ||
| Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs | Nao Hirokawa, Dohan Kim, Kiraku Shintani, René Thiemann | 31m |
Formalizes parallel critical pairs and the Gramlich/Toyama/Shintani–Hirokawa criteria in Isabelle, replacing a messy position-based notion with a context-based… | ||
| A Formalization of Complete Discrete Valuation Rings and Local Fields | María Inés de Frutos-Fernández | 27m |
Formalization uses 8,000 lines of Lean 3 and mathlib to encode discrete valuations, show the unit ball is a discrete valuation ring and conversely build the… | ||
| Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture | Siddhartha Gadgil, Anand Rao Tadipatri | 30m |
Formalization in Lean 4 reproduces Giles Gardam’s counterexample to Kaplansky’s Unit Conjecture by building an explicit metabelian group P (K = Z^3, Q =… | ||
| Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Argument... | Joseph Eremondi | 33m |
Claims a refinement called Strictly Monotone Brouwer trees (SMB-trees) that makes Brouwer-tree ordinals algebraically well behaved so the join distributes over… | ||
| Improved Assistance for Interactive Proof | Cezary Kaliszyk | 01h 03m |
Classifies learning tasks for ITPs and shows concrete wins: simple premise selection (k‑NN) raises Isabelle hammer success from ~38% to ~47%, graph neural nets… | ||
| Martin-Löf à la Coq | Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet | 30m |
A Coq formalization of Martin-Löf Type Theory (MLTT) that mechanizes its metatheory and proves decidability of conversion and of type checking using… | ||
| Displayed Monoidal Categories for the Semantics of Linear Logic | Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert | 30m |
Formalized a reusable library of monoidal-category constructions in UniMath using new displayed monoidal categories that let complicated monoidal structures be… | ||
| Univalent Double Categories | Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North | 27m |
Formalization builds two equivalent definitions of double categories: an unfolded explicit version and a structured version using two-sided displayed… | ||
| Formalizing the ∞-categorical Yoneda lemma | Nikolai Kudasov, Emily Riehl, Jonathan Weinberger | 34m |
Formalizes the ∞-categorical Yoneda lemma inside a new proof assistant called Rzk proof assistant (open source, VS Code plugin) using Riehl–Shulman’s… | ||
| Compositional Verification of Concurrent C Programs with Search Structure Templat... | Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang | 27m |
Implements Krishna et al.’s search-structure templates inside Verified Software Toolchain (VST) to prove C implementations of fine-grained concurrent search… | ||
| Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio... | Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey | 27m |
Provides a library of definitions, lemmas and proof rules that let one switch between array and tree views (mutually derivable) to localize updates, formalizes… | ||
| Unification for Subformula Linking under Quantifiers | Ike Mulder, Robbert Krebbers | 26m |
Proposes Quantifying on the Uninstantiated, a unification-based algorithm that retroactively turns Evars found during matching into existential quantifiers, so… | ||
| Lean Formalization of Extended Regular Expression Matching with Lookarounds | Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner | 28m |
Formalizes an extended regular‑expression matcher in Lean 4 formalization that models predicates with an effective Boolean algebra, represents positions as… | ||
| Memory simulations, security and optimization in a verified compiler | David Monniaux | 28m |
CompCert receives three new, machine-checked transformations: implemented and proved stack canaries and pointer authentication as security inserts, and a… | ||
| PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr... | Clément Chavanon, Frédéric Besson, Tristan Ninet | 31m |
A verified compiler for stateless firewall policies compiles a rule list into ordered reduced BDDs, applies BDD restriction to drop infeasible paths, uses an… | ||
| nothing matches | ||