The Vampire Diary
Laura Kovács, Vienna University of Technology, Austria
Bio:
Laura Kovács is a full professor of computer science at the TU Wien, leading the automated program reasoning (APRe) group of the Formal Methods in Systems Engineering division. Her research focuses on the design and development of new theories, technologies, and tools for program analysis, with a particular focus on automated assertion generation, symbolic summation, computer algebra, and automated theorem proving. She is the co-developer of the Vampire theorem prover and a Wallenberg Academy Fellow of Sweden. Her research has also been awarded with four ERC grants and two Amazon Research Awards. She is actively engaged in disseminating computer science results to schools, while organising computer science workshops with school children at the TU Wien and in Austrian schools. Starting with May 2025, she is the president and steering committee chair of the ETAPS association, running the ETAPS conferences.
CSLib: Building a Platform for AI-assisted Formal Verification in Lean
Clark Barrett, Stanford University, USA
Bio:
Clark Barrett is the Mizuki Asano and Thomas McGrath Professor (Research) of Computer Science in the School of Engineering at Stanford University. Before coming to Stanford in 2016, he was an Associate Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University. His expertise is in automated reasoning and its applications. He was an early pioneer in satisfiability modulo theories, formal hardware verification, and neural network verification. More recently, he has also pioneered efforts on AI-assisted formal verification. He is the director of the Stanford Center for Automated Reasoning (Centaur), co-director of the Stanford Center for AI Safety, and a member of the CSLib steering committee. He is an ACM Fellow and a two-time winner of the Computer Aided Verification (CAV) award (2021, 2024).
TBD
Claire Xenia Wolf, YosysHQ, Austria
Bio:
Claire Xenia Wolf is the original author of Yosys and many of the other tools in the YosysHQ software ecosystem. As CTO, she serves as the technical lead at YosysHQ, guiding the team of engineers and driving the company’s software development projects.
Verifying Rust code with Verus
Travis Hance, Max Planck Institute for Software Systems, Germany
Bio:
Travis Hance is a postdoctoral researcher at the Max Planck Institute for Software Systems in Saarbrücken, Germany. He previously earned his PhD at Carnegie Mellon University under Bryan Parno. He studies the theory and practice of systems verification, especially concurrent systems, and has an interest in the application of programming language theory.
Travis enjoys studying complex, concurrent software and building up understanding of the correctness of such software. He has applied formal methods to verify a high-performance page cache and a prototype concurrent memory allocator, among others. Travis has a particular interest in Rust, due to its unique combination of features that make it well-suited for the verification of systems software, and he is a co-developer of Verus, a tool for verifying Rust code, focusing especially on its support for verified multi-threaded software and low-level libraries. He also works with concurrent separation logic, and he has developed the “Leaf” library, a framework for modular specifications of data structures that involve shared, read-only state, and “VerusBelt,” for establishing the theoretical foundations of Verus.
Abstract:
I will introduce Verus, an open-source, Rust-based verification tool aimed at concurrent software and systems software, which I develop together with a number of collaborators in academia and industry. Verus has spawned a number of publications on a range of verified systems, is already seeing industrial use at Microsoft and Amazon, and has been the subject of a number of experiments on generating proofs with AI.
In this tutorial, I will give an overview of Verus and what it can do, and why we invented it compared to the previous state-of-the-art approaches to program verification. I will give a tutorial on how to get started with Verus, and I will illustrate how we approach the various challenges of verification through a number of examples.