Formal verification provides unmatched correctness guarantees, but has traditionally required prohibitive manual effort. In this talk, I will present work that advances my vision of reducing the effort required for formal verification without compromising efficiency or trust. I will show how our Cogent language, with its ownership type system and certifying compiler, significantly reduced the cost of verifying efficient file systems. I will demonstrate how our declarative data layout language, Dargent, trivialised the development of verified device drivers. I will also talk about some of our work on memory-safety, multi-language interoperability, cost analysis, and reasoning about concurrent code. Looking ahead, I plan to extend these methods to further support reasoning about memory safety and concurrency, enable reasoning about emerging domains such as quantum programming, and simplify the verification of APIs and foreign function interfaces. The purpose of discussing such work in progress is to initiate collaboration on topics of potential common interest.

Christine Rizkallah is a Senior Lecturer at the School of Computing and Information Systems at the University of Melbourne in Australia. She received her PhD 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, and a Trustworthy Systems Postdoctoral position at NICTA. Her areas of expertise are formal methods and programming languages. 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, to prove that software systems are correct and secure. Over the past years, she has led the development of the Cogent and Dargent programming languages that ease the development of verified systems software. For her PhD, she created a framework for ensuring the correctness of results from algorithmic libraries and demonstrated her framework on the widely used LEDA algorithmic library.