| Publication | Date of Publication | Type |
|---|
| Foundational verification of stateful P4 packet processing | 2024-11-26 | Paper |
| Abstraction and subsumption in modular verification of C programs | 2024-03-14 | Paper |
| Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method | 2024-02-28 | Paper |
| A solver for arrays with concatenation | 2023-06-14 | Paper |
| Efficient extensional binary tries | 2023-06-14 | Paper |
| Bringing Order to the Separation Logic Jungle | 2022-12-09 | Paper |
| Verified Erasure Correction in Coq with MathComp and VST | 2022-12-07 | Paper |
| Connecting Higher-Order Separation Logic to a First-Order Outside World | 2022-10-13 | Paper |
| Abstraction and subsumption in modular verification of C programs | 2022-06-20 | Paper |
| C-language floating-point proofs layered with VST and Flocq | 2021-12-02 | Paper |
| Corrigendum: C floating-point proofs layered with VST and Flocq | 2021-12-02 | Paper |
| VST-Floyd: a separation logic tool to verify correctness of C programs | 2018-08-21 | Paper |
| Lambda-splitting | 2017-08-21 | Paper |
| Compositional CompCert | 2016-09-29 | Paper |
| A theory of indirection via approximation | 2015-06-11 | Paper |
| A semantic model of types and machine instructions for proof-carrying code | 2015-03-17 | Paper |
| Mostly Sound Type System Improves a Foundational Program Verifier | 2015-01-13 | Paper |
| A very modal model of a modern, major, general type system | 2014-09-12 | Paper |
| Program Logics for Certified Compilers | 2014-07-28 | Paper |
| Verified heap theorem prover by paramodulation | 2014-07-21 | Paper |
| Multimodal Separation Logic for Reasoning About Operational Semantics | 2014-05-13 | Paper |
| Verified Compilation for Shared-Memory C | 2014-04-16 | Paper |
| A list-machine benchmark for mechanized metatheory (extended abstract) | 2014-01-10 | Paper |
| Efficient Substitution in Hoare Logic Expressions | 2013-05-10 | Paper |
| A list-machine benchmark for mechanized metatheory | 2013-04-17 | Paper |
| A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow | 2012-06-29 | Paper |
| Verified Software Toolchain | 2011-05-19 | Paper |
| Formal Verification of Coalescing Graph-Coloring Register Allocation | 2010-05-04 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
| Separation Logic for Small-Step cminor | 2008-09-02 | Paper |
| Oracle Semantics for Concurrent Separation Logic | 2008-04-11 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2007-02-12 | Paper |
| Dependent types ensure partial correctness of theorem provers | 2004-09-27 | Paper |
| Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf | 2004-09-24 | Paper |
| A trustworthy proof checker | 2004-08-06 | Paper |
| Modern Compiler Implementation in Java | 2003-06-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723406 | 2001-07-05 | Paper |
| Shrinking lambda expressions in linear time | 1998-08-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4379577 | 1998-03-02 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4343027 | 1997-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4343028 | 1997-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3026313 | 1987-01-01 | Paper |
| Generalizations of the sethi‐ullman algorithm for register allocation | 1987-01-01 | Paper |
