News 2024

Distributed, Networked & Mobile Systems

MPI-SWS researchers receive SOSP'24 Distinguished Artifact Award

November 2024
Homepage News, Other Awards and Prizes
MPI-SWS research group leader Andrea Lattuada and postdoctoral fellow Travis Hance, who has recently joined Andrea’s Principled Systems group, have received, along with their collaborators, the SOSP'24 Distinguished Artifact Award for their paper "Verus: A Practical Foundation for Systems Verification."

Traditional software testing methods will reveal bugs, but testing alone can’t guarantee the absence of errors. Software verification tools such as Verus mathematically prove that software behaves according to its specifications. ...
MPI-SWS research group leader Andrea Lattuada and postdoctoral fellow Travis Hance, who has recently joined Andrea’s Principled Systems group, have received, along with their collaborators, the SOSP'24 Distinguished Artifact Award for their paper "Verus: A Practical Foundation for Systems Verification."


Traditional software testing methods will reveal bugs, but testing alone can’t guarantee the absence of errors. Software verification tools such as Verus mathematically prove that software behaves according to its specifications. Verus is a tool for verifying the correctness of code written in Rust. Developers write specifications of what their code should do, and Verus statically checks that the executable Rust code will always satisfy the specifications for all possible executions of the code.


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.


 
Read more

Andrea Lattuada joins MPI-SWS faculty

September 2024
Homepage News, New faculty
Andrea Lattuada will join MPI-SWS as a Research Group Leader in September 2024. Before joining MPI-SWS, Andrea worked as a researcher in the VMware Research Group. He completed his PhD at ETH Zurich, where he focused on systems for distributed data processing and systems software verification.

Andrea builds verification tools and formally verified systems with a focus on pragmatism. He co-started and co-leads the Verus project. Verus is a tool used by various industry and academic projects to rapidly verify the correctness of systems code written in Rust. ...
Andrea Lattuada will join MPI-SWS as a Research Group Leader in September 2024. Before joining MPI-SWS, Andrea worked as a researcher in the VMware Research Group. He completed his PhD at ETH Zurich, where he focused on systems for distributed data processing and systems software verification.

Andrea builds verification tools and formally verified systems with a focus on pragmatism. He co-started and co-leads the Verus project. Verus is a tool used by various industry and academic projects to rapidly verify the correctness of systems code written in Rust. At MPI, his research group will continue to leverage software verification to substantially improve the safety and reliability of systems software. This will involve developing new and more powerful techniques to reason about complex software, improving the usability and efficiency of verification tools, and devising principled and cost-effective development disciplines for verified software. Andrea also collaborates with researchers at ETH Zürich on new programming models for the cloud, and on building a verified operating system with a compact, well-specified programming interface.

Andrea’s group has open positions for doctoral students, postdocs, and interns who are interested in working on systems software verification. Current projects focus on making verification more practical and usable by engineers and on leveraging advanced reasoning techniques to tackle complex software. Andrea’s website has more details on his research profile.
Read more

Operating Systems course at Saarland University

April 2024
Courses
The Summer 2024 core Operating Systems course at Saarland University is being co-taught by MPI-SWS faculty members Antoine Kaufmann and Laurent Bindschaedler along with Yiting Xia from MPI-INF.