A key challenge in computer science research is to establish that programs and compilers behave correctly. We tackle this challenge by showing that a formal description of a program or a system exhibits a set of well-defined properties through research that involves algorithms, complexity, logic, and semantics.
This focus area is closely related to our Formal Structures theme, but focuses more on tool implementations and the application of logic to programs and programming languages. Our goal is to scale program verification techniques to challenging programming paradigms such as fine-grained/lock-free concurrency, message-passing concurrency, higher-order functions, modules, and substructural/linear types. We develop semantics of programming languages such as C, Rust, and Scala, and use these semantics to verify properties such as type safety, functional correctness, deadlock freedom, non-interference, and compiler correctness. A key ingredient is the use of program logics, in particular concurrent separation logic, to reason about programs at a suitable level of abstraction.
We implement and verify most of our techniques and theory in the Rocq prover using the Iris framework for higher-order concurrent separation logic. We study both interactive (human-guided) and mostly-automated techniques.