| 2026 | CPP | Building Blocks for Step-Indexed Program Logics. | Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gher, Robbert Krebbers |
| 2026 | CPP | A Recipe for Modular Verification of Generic Tree Traversals. | Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg |
| 2025 | ITP | Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. | Robbert Krebbers, Luko van der Maas, Enrico Tassi |
| 2025 | PPDP | Mechanized Type Soundness for Substructural Types using Iris. | Robbert Krebbers |
| 2024 | CPP | Unification for Subformula Linking under Quantifiers. | Ike Mulder, Robbert Krebbers |
| 2024 | ITP | Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. | Marc Hermes, Robbert Krebbers |
| 2023 | ITP | Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). | Robbert Krebbers |
| 2022 | PLDI | Diaframe: automated verification of fine-grained concurrent programs in Iris. | Ike Mulder, Robbert Krebbers, Herman Geuvers |
| 2021 | CPP | Machine-checked semantic session typing. | Jonas Kastberg Hinrichsen, Danil Louwrink, Robbert Krebbers, Jesper Bengtson |
| 2021 | PLDI | RefinedC: automating the foundational verification of C code with refined ownership types. | Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg |
| 2021 | PLDI | Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. | Simon Spies, Lennard Gher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal |
| 2021 | SP | Compositional Non-Interference for Fine-Grained Concurrent Programs. | Dan Frumin, Robbert Krebbers, Lars Birkedal |
| 2020 | CPP | Intrinsically-typed definitional interpreters for linear, session-typed languages. | Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser |
| 2019 | ESOP | Semi-automated Reasoning About Non-determinism in C Expressions. | Dan Frumin, Lon Gondelman, Robbert Krebbers |
| 2018 | LICS | ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. | Dan Frumin, Robbert Krebbers, Lars Birkedal |
| 2017 | ESOP | The Essence of Higher-Order Concurrent Separation Logic. | Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal |
| 2017 | POPL | Interactive proofs in higher-order concurrent separation logic. | Robbert Krebbers, Amin Timany, Lars Birkedal |
| 2016 | ICFP | Higher-order ghost state. | Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer |
| 2015 | CPP | A Typed C11 Semantics for Interactive Theorem Proving. | Robbert Krebbers, Freek Wiedijk |
| 2014 | ITP | Formal C Semantics: CompCert and the C Standard. | Robbert Krebbers, Xavier Leroy, Freek Wiedijk |
| 2014 | POPL | An operational and axiomatic semantics for non-determinism and sequence points in C. | Robbert Krebbers |
| 2013 | CPP | Aliasing Restrictions of C11 Formalized in Coq. | Robbert Krebbers |
| 2013 | FOSSACS | Separation Logic for Non-local Control Flow and Block Scope Variables. | Robbert Krebbers, Freek Wiedijk |