| 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
Lecture Notes in Computer Science | 2024-02-28 | Paper |
A solver for arrays with concatenation
Journal of Automated Reasoning | 2023-06-14 | Paper |
Efficient extensional binary tries
Journal of Automated Reasoning | 2023-06-14 | Paper |
Bringing Order to the Separation Logic Jungle
Programming Languages and Systems | 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
Programming Languages and Systems | 2022-10-13 | Paper |
Abstraction and subsumption in modular verification of C programs
Formal Methods in System Design | 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
Journal of Automated Reasoning | 2018-08-21 | Paper |
Lambda-splitting: a higher-order approach to cross-module optimizations
Proceedings of the second ACM SIGPLAN international conference on Functional programming | 2017-08-21 | Paper |
Compositional CompCert
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-09-29 | Paper |
A theory of indirection via approximation
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
A semantic model of types and machine instructions for proof-carrying code
Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
Mostly sound type system improves a foundational program verifier
Certified Programs and Proofs | 2015-01-13 | Paper |
A very modal model of a modern, major, general type system
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
| Program logics for certified compilers | 2014-07-28 | Paper |
Verified heap theorem prover by paramodulation
Proceedings of the 17th ACM SIGPLAN international conference on Functional programming | 2014-07-21 | Paper |
Multimodal Separation Logic for Reasoning About Operational Semantics
Electronic Notes in Theoretical Computer Science | 2014-05-13 | Paper |
Verified Compilation for Shared-Memory C
Programming Languages and Systems | 2014-04-16 | Paper |
| A list-machine benchmark for mechanized metatheory (extended abstract) | 2014-01-10 | Paper |
Efficient substitution in Hoare logic expressions
Electronic Notes in Theoretical Computer Science | 2013-05-10 | Paper |
A list-machine benchmark for mechanized metatheory
Journal of Automated Reasoning | 2013-04-17 | Paper |
A certificate infrastructure for machine-checked proofs of conditional information flow
Lecture Notes in Computer Science | 2012-06-29 | Paper |
Verified software toolchain (invited talk)
Programming Languages and Systems | 2011-05-19 | Paper |
Formal verification of coalescing graph-coloring register allocation
Programming Languages and Systems | 2010-05-04 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Separation Logic for Small-Step cminor
Lecture Notes in Computer Science | 2008-09-02 | Paper |
Oracle Semantics for Concurrent Separation Logic
Programming Languages and Systems | 2008-04-11 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Dependent types ensure partial correctness of theorem provers
Journal of Functional Programming | 2004-09-27 | Paper |
Polymorphic lemmas and definitions in \lambdaProlog and Twelf
Theory and Practice of Logic Programming | 2004-09-24 | Paper |
A trustworthy proof checker
Journal of Automated Reasoning | 2004-08-06 | Paper |
| Modern Compiler Implementation in Java | 2003-06-25 | Paper |
| scientific article; zbMATH DE number 1614684 (Why is no real title available?) | 2001-07-05 | Paper |
Shrinking lambda expressions in linear time
Journal of Functional Programming | 1998-08-03 | Paper |
| scientific article; zbMATH DE number 1122795 (Why is no real title available?) | 1998-03-02 | Paper |
| scientific article; zbMATH DE number 1027560 (Why is no real title available?) | 1997-06-29 | Paper |
| scientific article; zbMATH DE number 1027561 (Why is no real title available?) | 1997-06-29 | Paper |
| scientific article; zbMATH DE number 4013996 (Why is no real title available?) | 1987-01-01 | Paper |
Generalizations of the sethi‐ullman algorithm for register allocation
Software: Practice and Experience | 1987-01-01 | Paper |
