CPP 2025
22 papers
- A CHERI C Memory Model for Verified Temporal Safety
- An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
- An Isabelle/HOL Framework for Synthetic Completeness Proofs
- CRIS: The Power of Imagination in Specification and Verification (Invited Talk)
- CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
- Certifying Rings of Integers in Number Fields
- Formalization of Differential Privacy in Isabelle/HOL
- Formalized Burrows-Wheeler Transform
- Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
- Formalizing the One-Way to Hiding Theorem
- Formally Verified Hardening of C Programs against Hardware Fault Injection
- Further Tackling Post Correspondence Problem and Proof Generation
- Intrinsically Correct Sorting in Cubical Agda
- Leakage-Free Probabilistic Jasmin Programs
- Machine Checked Proofs and Programs in Algebraic Combinatorics
- Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
- Nominal Matching Logic with Fixpoints
- Prospects for Computer Formalization of Infinite-Dimensional Category Theory (Invited Talk)
- Split Decisions: Explicit Contexts for Substructural Languages
- Tactic Script Optimisation for Aesop
- The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
- Verified and Efficient Matching of Regular Expressions with Lookaround