Talk: Automated and Foundational Verification of Low-Level Programs
Michael Sammler: PhD Student, Max Planck Institute for Software Systems
LIVE STREAM: https://uwmadison.zoom.us/j/93599508194?pwd=T1NnR3ptb1Q3czA3bXNIR3Aya0pOUT09
Abstract: The correctness of low-level software like operating systems or
hypervisors is crucial to the reliability and security of modern
applications. This makes such low-level programs a prime target for
formal verification. However, to apply formal verification to
low-level software, we must deal with three challenges:
1) handling realistic systems code and programming languages, which is
often idiomatic and nuanced,
2) ensuring the soundness of the verification technique, ideally via
foundational proofs in a proof assistant, and
3) automating the verification as much as possible.
In this talk, I present my work and my vision towards
advancing formal verification along these dimensions simultaneously.
Concretely, the talk focuses on RefinedC, a new approach to verifying
C code that combines foundational proofs with a high degree of
automation. RefinedC achieves this via a novel combination of
refinement and ownership types, and a new backtracking-free proof
search procedure for separation logic. I also outline my vision that
uses RefinedC as the center piece of a unified foundational framework
for verifying realistic multi-language programs (e.g., programs
written in C and assembly).
Bio: Michael Sammler is a PhD student at the Max Planck Institute for Software Systems under the supervision of Deepak Garg and Derek Dreyer. His research focuses on developing techniques for formal verification of realistic low-level systems software that combine machine-checked proofs with a high degree of automation. He has received multiple awards for his research, including Distinguished Paper awards at PLDI, POPL, and USENIX Security, and a Google PhD fellowship.