Derek Dreyer

Lightweight verification of separate compilation

2016

Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of …

VIP: verifying real-world C idioms with integer-pointer casts

2022 · Proceedings of the ACM on Programming Languages

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level ( e.g. , bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they …

DimSum: A Decentralized Approach to Multi-language Semantics and Verification

2023 · Proceedings of the ACM on Programming Languages

Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language …

Data Race Freedom à la Mode

2025 · Proceedings of the ACM on Programming Languages

We present DRFCaml, an extension of OCaml’s type system that guarantees data race freedom for multithreaded OCaml programs while retaining backward compatibility with existing sequential OCaml code. We build on recent work of Lorenzen et …