Formal Methods For Efficient, Reliable Systems Programming -
Compilers are foundational—applications can only be as efficient and reliable as the underlying compiler stack that translates their logic to machine code. But compiler expertise is a finite resource, and engineers may have to choose whether to prioritize adding optimizations for efficiency or validating the compiler features they already have for reliability. In this talk, I’ll show how my work pushes past this tension between performance and correctness by applying practical formal methods. I’ll describe our Diospyros compiler for an energy-efficient embedded system, which uses automated reasoning over equalities to produce fast code with less manual programming effort. I will then show how our Kani verifier for Rust leverages compiler invariants to speed up correctness checks for low-level systems code. Finally, I’ll address my ongoing work toward verifying machine code generation in a popular production compiler infrastructure and outline my goals for raising the level of abstraction in building efficient and reliable compilers for computer systems.

Bio:
Alexa VanHattum is a PhD candidate in Computer Science at Cornell advised by Adrian Sampson and an NSF Graduate Research Fellow. Her research sits at the intersection of programming languages and systems, with a focus on applying formal methods to the compiler stack. Before Cornell, she worked on health software at Apple and received her ScB in Computer Science from Brown University.