Room 206 (2nd floor, badged access)
9 November 2026 - 14h00
Towards Facilitating Verification across Language Boundaries
by Christine Rizkallah from Université de Melbourne
invited by David MONNIAUX
9 November 2026 - 14h00
Towards Facilitating Verification across Language Boundaries
by Christine Rizkallah from Université de Melbourne
invited by David MONNIAUX
Abstract: Software verification is essential for building secure and reliable systems. Landmark projects such as the verified seL4 microkernel and the verified CompCert compiler have pushed the boundaries of what is considered feasible in our field. However, many critical software components remain unverified, and important properties beyond the correctness of sequential code still require attention. Verifying such systems using existing brute-force techniques would be infeasible. Instead, my research focuses on reducing the manual effort required to verif software within interactive theorem provers, without compromising performance or trust.
In this talk, I will present several lines of work that advance this goal across various settings. I will first briefly start by demonstrating how our Cogent language, through its uniqueness type system and certifying compiler, facilitated the development of trustworthy file systems. While safe languages such as Cogent, Swift, and Rust prevent memory-safety errors and support refinement from functional code into efficient imperative code, they often limit low-level control over memory layouts. To address this limitation, I will present our declarative data-layout specification language extension, Dargent, which enables Cogent programmers to regain fine-grained control over memory layouts. This approach trivialised the verification of low-level systems components, such as device drivers, down to the bit level. Even with such extension, safe languages still limit expressivity and therefore, typically rely on foreign-function interfaces to interoperate with performance-critical components written in unsafe languages such as C or unsafe Rust, where formal verification remains more challenging. Since real-world systems span multiple programming languages, we have ongoing efforts that aim to ease verification across programming language boundaries. In particular, we demonstrate how separation logic can be used to discharge uniqueness-type obligations, bridging reasoning principles between type-safe components and components where safety requires manual proofs. Finally, I will briefly outline ongoing work on easing the cost analysis of lazy functional programs and on developing logical frameworks that extend safety guarantees to information-flow security, including for concurrent systems.
