Software verification is essential for building secure systems. Successful formal verification projects such as the seL4 microkernel and the CompCert C compiler have pushed the boundary of what is deemed feasible in our field. However, many critical software components still remain unverified. Verifying such components using the existing brute-force techniques is infeasible. Instead, my research vision involves creating methods to reduce the cost of verification without compromising on efficiency or trust. In this talk, I will present work that achieves this vision within several different areas in computer science. I will start by presenting the Cogent languages and emphasising how its uniqueness type system and certifying compiler dramatically reduced the cost of verifying efficient filesystems.Then I will introduce Dargent, a data layout specification language that we developed to automate a large portion of the formal verification of device drivers. Finally, I will end by highlighting promising next steps for further simplifying formal software verification.

Bio: Christine Rizkallah is a Senior Lecturer at the School of Computing and Information Systems at the University of Melbourne in Australia. She received her Ph.D. in Computer Science from Saarland University and the Max-Planck Institute for Informatics. Rizkallah previously held a Lecturer position at UNSW Sydney, a DeepSpec Postdoctoral position at the University of Pennsylvania, a Trustworthy Systems Postdoc position at NICTA. Her research interests include formal methods, programming languages, and security. Her research focuses on using programming language techniques, such as type systems and certifying compilers, along with interactive theorem provers, such as Coq and Isabelle/HOL, for proving that software systems are correct and secure. Over the past five years, she has lead the development of the Cogent and Dargent programming languages which ease the development of verified software systems.