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.
|Lasagne: A Static Binary Translator for Weak Memory Model Architectures|
NotesSome rough ideas. Feel free to e-mail me with comments or questions.
|Mar. 2022||Optimal Cost is Monotonic over Preconditions|
|Mar. 2022||Tutorial: Docker for Research Artifacts|
|Mar. 2021|| Superoptimization of WebAssembly Process Graphs|
UU Colloquium, MSc Thesis Defense