Concurrent and distributed programs that form the infrastructure of online services, e.g., online banking, power grid control, government services, are notoriously difficult to design and implement. This is in part due to the sheer scale of software components that run in parallel and interact with one another. Our research focuses on developing program logics, techniques based on mathematical logic designed for formal reasoning about these systems and proving their correctness. The state-of-the-art program logic in this area of research is Iris: a higher-order concurrent separation logic framework, implemented and proven sound in the Rocq proof assistant. Iris is a collaborative project between multiple universities, with Aarhus University being one of the main contributors. It has been used to reason about a wide range of systems (ranging from distributed higher-order concurrent imperative programs to the low-level assembly language of capability machine programs) and wide range of correctness properties (safety, liveness, probabilistic properties, and security properties). 

Iris has been used in industry, e.g., by researchers at Facebook/Meta and by start-up company Bedrock systems.  Moreover, it has been used to verify essential properties of the Rust programming language, the OCaml programming language, and Web Assembly. It has also been used to study low-level hardware security and privacy guarantees offered by so-called capability machines, the next generation of processors.