Inaugural Lecture: Samara Ren and Michael Sammler
Samara's Talk Title: "Computational Inverse Design of Shape-Morphing Structures"
Michael's Talk Title: "Automated and Foundational Verification of Low-Level Programs"
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.