Career chat and Tech talk with Professor Alexa VanHattum

Technical Talk: Lightweight, Modular Verification for Instruction Selection
Language-level guarantees—like runtime isolation for WebAssembly modules—are only as strong as the compiler that produces a native-machine-specific executable. Subtle wrong-code bugs in native instruction selection can introduce serious security flaws. In this talk, I’ll describe VeriISLE, our system for lightweight, modular verification of instruction-lowering rules in Cranelift, a production retargetable WebAssembly code generator. VeriISLE reproduces known bugs (including a 9.9/10 severity security bug) and identifies previously-unknown bugs and underspecified compiler invariants. More broadly, I’ll discuss how integrating lightweight formal methods can free engineers from having to choose between prioritizing efficiency and correctness.

We will then have an Ask Me Anything session where I will be happy to answer questions on my research, the academic job market (especially teaching- and undergraduate-focused positions), and collaboration between academia and industry.