Principled Systems Logo Principled Systems Group

Max Planck Institute for Software Systems

The Principled Systems Group at the Max Planck Institute for Software Systems (MPI-SWS) is led by Andrea Lattuada. We design, implement, and verify systems software, construed broadly[1] and focus on the advancement of verification tooling and methodology for systems verification.

We are interested in systems software verification as a way to substantially improve their safety and reliability, but to achieve this, the verification effort must be commensurate to the value it provides. We build (verified) systems, and extend the available tooling to find and fix inefficiencies.

Contact: (click to reveal)@mpi-sws.org

Verus Logo We co-lead the Verus project, Verus is a tool to rapidly verify the correctness of systems code written in Rust. The Verus project involves members from VMware Research, Microsoft Research, Carnegie Mellon University, ETH Zurich, University of Washington, University of Michigan, University of Wisconsin-Madison, and others. There are a number of research and industry projects using and developing Verus: verus-lang.github.io/verus/publications-and-projects/.

Lectures offered at Saarland University

  • Formal Verification of Systems Software (Winter Semester 2024/2025): The course teaches how to formally verify systems software that underpins computing infrastructure using Rust and the Verus verification framework to ensure implementations match their abstract models and remain bug-free. By learning to model system behavior and write proofs with the help of SMT solvers, students gain the skills to design, implement, and verify distributed systems, which can prevent costly failures like data loss and service outages.
January 2025

Postdoctoral researcher Travis Hance and research intern Alexander Bai joined the group

Travis has recently earned his Ph.D. from Carnegie Mellon University under Bryan Parno, with work spanning systems, verification tools, and large verification projects. Travis is part of the Verus core team.

Alex recently finished his undergraduate studies at Tufts University majoring in computer science and mathematics, advised by Jeff Foster and David Smyth. Alex has contributed to Verus' internals and to its standard library.

November 2024

Andrea Lattuada and Travis Hance receive SOSP'24 distinguised artifact award

Group leader Andrea Lattuada and postdoctoral researcher Travis Hance, who has recently joined the group, have received, along with their collaborators, the SOSP'24 Distinguished Artifact Award for their paper "Verus: A Practical Foundation for Systems Verification."

The artifact, available at https://verus-lang.github.io/paper-sosp24-artifact/, contains the code and proof for 5 sizable case studies, comprising over six thousand lines of executable code, verified with around 35 thousand lines of proof and specification code, and a number of smaller verification benchmarks. In combination, these help demonstrate Verus’ ability to quickly verify complex systems in multiple domains: from operating systems, to critical runtime components, to distributed systems.

Members

Andrea Lattuada

Group Leader

Website

Travis Hance

Postdoctoral Researcher

Website

Alexander Bai

Research Intern

Website

Abigail Pribisova

CS@max planck
Doctoral Student
Research Immersion Lab

Website

Aaron Bies

Master Student at UdS
Research Assistant

Affiliated Researchers and Collaborators

Matthias Brun

PhD Student
Assistant Researcher
ETH Zurich

Website

Laila Elbeheiry

PhD Student
Foundations of Programming
MPI-SWS

Website

Reto Achermann

Assistant Professor
Systopia Lab
University of British Columbia

Website

Johanna Polzin

Bachelor Student in Computer Science
ETH Zurich

Website

Recent Peer-reviewed Publications

[1] Inspired by Systopia's definition of the scope of Systems research.