Dennis Sprokholthe / himd.g.sprokholt [at] tudelft.nlsourcedennis@email@example.comMScMaleTU DelftPhD CandidateNetherlandsEnglish, Dutch
In my research, I apply formal methods to low-level programs. I am interested in superoptimization, where I perform automated reasoning to construct correct and near-optimal programs from first principles. Often, you'll find me writing mechanized proofs in Agda or fast programs in Rust.
|Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures
|Lasagne: A Static Binary Translator for Weak Memory Model Architectures
NotesSome rough ideas. Feel free to e-mail me with comments or questions.
|Dependency Injection in Rust
|Galois Connections on Lattices
|Agda, Full Adders, and Flags
|Optimal Cost is Monotonic over Preconditions
|Tutorial: Docker for Research Artifacts