| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Azalea Raad |
Under-Approximation for Scalable Bug Detection (Keynote).  |
CPP  |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang |
Compositional Verification of Concurrent C Programs with Search Structure Templates. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | David Monniaux |
Memory Simulations, Security and Optimization in a Verified Compiler. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Ike Mulder, Robbert Krebbers |
Unification for Subformula Linking under Quantifiers. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Nao Hirokawa, Dohan Kim 0001, Kiraku Shintani, René Thiemann |
Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Chelsea Edmonds, Lawrence C. Paulson |
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur 0001, Ilya Sergey |
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Eremondi |
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North |
Univalent Double Categories. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolai Kudasov, Emily Riehl, Jonathan Weinberger |
Formalizing the ∞-Categorical Yoneda Lemma. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel, Ariel Kellison |
VCFloat2: Floating-Point Error Analysis in Coq. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy (eds.) |
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet |
Martin-Löf à la Coq. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Ian Shillito, Dominik Kirst |
A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Siddhartha Gadgil, Anand Rao Tadipatri |
Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Lauren White, Laura Titolo, J. Tanner Slagel, César A. Muñoz |
A Temporal Differential Dynamic Logic Formal Embedding. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert |
Displayed Monoidal Categories for the Semantics of Linear Logic. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner |
Lean Formalization of Extended Regular Expression Matching with Lookarounds. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | Clément Chavanon, Frédéric Besson, Tristan Ninet |
PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. |
CPP |
2024 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Cyril Cohen, Ayumu Saito |
Semantics of Probabilistic Programs using s-Finite Kernels in Coq. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Hugo Férée, Sam van Gool |
Formalizing and Computing Propositional Quantifiers. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Anthony Bordg, Adrián Doña Mateo |
Encoding Dependently-Typed Constructions into Simple Type Theory. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Kexing Ying, Rémy Degenne |
A Formalization of Doob's Martingale Convergence Theorems in mathlib. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi 0001 |
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Jannis Limperg, Asta Halkjær From |
Aesop: White-Box Best-First Proof Search for Lean. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds |
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Yannick Forster 0002, Felix Jahn, Gert Smolka |
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Cezary Kaliszyk |
Improved Assistance for Interactive Proof (Keynote). |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Katherine Kosaian, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandrine Blazy |
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy |
ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Lamiaux, Axel Ljungström, Anders Mörtberg |
Computing Cohomology Rings in Cubical Agda. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Bhavik Mehta |
Formalising Sharkovsky's Theorem (Proof Pearl). |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Christina Kohl, Aart Middeldorp |
A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic (eds.) |
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Floris van Doorn, Patrick Massot, Oliver Nash |
Formalising the h-Principle and Sphere Eversion. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen |
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Valentin Blot, Denis Cousineau 0002, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial |
Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Färber 0002 |
Terms for Efficient Proof Checking and Parsing. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Brae J. Webb, Ian J. Hayes, Mark Utting |
Verifying Term Graph Optimizations using Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua Clune |
A Formalized Reduction of Keller's Conjecture. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub |
A Formal Disproof of Hirsch Conjecture. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Yann Herklotz, Delphine Demange, Sandrine Blazy |
Mechanised Semantics for Gated Static Single Assignment. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Eske Hoy Nielsen, Danil Annenkov, Bas Spitters |
Formalising Decentralised Exchanges in Coq. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 1 | Louis Cheung, Liam O'Connor, Christine Rizkallah |
Overcoming restraint: composing verification of foreign functions with cogent. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
A verified algebraic representation of cairo program execution. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | César Muñoz |
Structural embeddings revisited (invited talk). |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | William Schultz, Ian Dardik, Stavros Tripakis |
Formal verification of a distributed dynamic reconfiguration protocol. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle |
A compositional proof framework for FRETish requirements. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Patricia Johann, Enrico Ghiorzi |
(Deep) induction rules for GADTs. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Dan Frumin |
Semantic cut elimination for the logic of bunched implications, formalized in Coq. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark Koch, Dominik Kirst |
Undecidability, incompleteness, and completeness of second-order logic in Coq. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Pablo Donato, Pierre-Yves Strub, Benjamin Werner |
A drag-and-drop proof tactic. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino |
Formally verified superblock scheduling. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonathan Prieto-Cubides |
On homotopy of walks and spherical maps in homotopy type theory. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt |
Forward build systems, formally. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Oliver Nash |
Formalising lie algebras. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Denis Firsov, Dominique Unruh |
Reflection, rewinding, and coin-toss in EasyCrypt. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | June Andronick |
The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Benedikt Ahrens, Ralph Matthes, Anders Mörtberg |
Implementing a category-theoretic framework for typed abstract syntax. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Ambal, Sergueï Lenglet, Alan Schmitt |
Certified abstract machines for skeletal semantics. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Mihails Milehins |
An extension of the framework types-to-sets for Isabelle/HOL. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Derek Egolf, Sam Lasser, Kathleen Fisher |
Verbatim++: verified, optimized, and semantically rich lexing with derivatives. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrei Popescu 0001, Steve Zdancewic (eds.) |
CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrew W. Appel |
Coq's vibrant ecosystem for verification engineering (invited talk). |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Hing-Lun Chan |
Windmills of the minds: an algorithm for fermat's two squares theorem. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli |
Applying formal verification to microkernel IPC at meta. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Färber 0002 |
Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Friis Vindum, Dan Frumin, Lars Birkedal |
Mechanized verification of a fine-grained concurrent queue from meta's folly library. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Ariel Kellison |
A machine-checked direct proof of the Steiner-lehmus theorem. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader |
CertiStr: a certified string solver. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Moine 0001, Arthur Charguéraud, François Pottier |
Specification and verification of a transient stack. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 1 | Elliot Catt, Michael Norrish |
On the formalisation of Kolmogorov complexity. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | C. H. R. Chhak, Andrew Tolmach, Sean Noble Anderson |
Towards formally verified compilation of tag-based policy enforcement. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini |
A Coq formalization of data provenance. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Teaching algorithms and data structures with a proof assistant (invited talk). |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Desharnais, Stefan Brunthaler 0001 |
Towards efficient and verified virtual machines for dynamic languages. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. |
Formal verification of authenticated, append-only skip lists in Agda. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Kirst, Felix Rech |
The generalised continuum hypothesis implies the axiom of choice in Coq. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Jannis Limperg |
A novice-friendly induction tactic for lean. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Johan Commelin, Robert Y. Lewis |
Formalizing the ring of Witt vectors. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Lööw |
Lutsig: a verified Verilog compiler for verified circuit development. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Max W. Haslbeck, René Thiemann |
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Sophie Tourret, Jasmin Blanchette |
A modular Isabelle framework for verifying saturation provers. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Jason Z. S. Hu, Jacques Carette |
Formalizing category theory in Agda. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Friis Vindum, Lars Birkedal |
Contextual refinement of the Michael-Scott queue (proof pearl). |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Tanner Slagel, Lauren White, Aaron Dutle |
Formal verification of semi-algebraic sets and real analytic functions. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Olivier Laurent 0001 |
An anti-locally-nameless approach to formalizing quantifiers. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee 0001, Jean-Baptiste Tristan |
A formal proof of PAC learnability for decision stumps. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton |
CertRL: formalizing convergence proofs for value and policy iteration in Coq. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters |
Extracting smart contracts tested and verified in Coq. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Catalin Hritcu, Andrei Popescu 0001 (eds.) |
CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021 |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Sewell |
Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 1 | Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar |
Lassie: HOL4 tactics by example. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license