Dennis Sprokholthe / himd.g.sprokholt [at] tudelft.nlsourcedennissourcedennisMScMaleTU 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.
|ASPLOS '23||Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures|
|PLDI'22||Lasagne: A Static Binary Translator for Weak Memory Model Architectures|
NotesSome rough ideas. Feel free to e-mail me with comments or questions.
|Aug. '22||Galois Connections on Lattices|
|Jul. '22||Agda, Full Adders, and Flags|
|Mar. '22||Optimal Cost is Monotonic over Preconditions|
|Mar. '22||Tutorial: Docker for Research Artifacts|
|Mar. '21|| Superoptimization of WebAssembly Process Graphs|
UU Colloquium, MSc Thesis Defense