Faculty
Dr. Swen Jacobs a faculty at CISPA, where he leads the Rigorous Analysis and Design group. From 2014 until 2018, he led a research group within the Reactive Systems Group at Saarland University. Before that, Swen was a postdoctoral researcher at TU Graz (with Roderick Bloem) and at EPFL (with Viktor Kuncak), and was a visiting professor at the University of Ljubljana. He obtained his doctorate from Saarland University in 2010, based on work he did at the Max Planck Institute for Informatics.
FMCAD
FMCAD 2022Formal Methods in Computer-Aided Design 2022
OOPSLA
PACMPLOOPSLA 2021
CAV
Computer Aided Verification - 33nd International Conference, CAV 202133rd International Conference on Computer-Aided Verification
CAV
Computer Aided Verification - 32nd International ConferenceComputer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I
CAV
CAV 2020
VMCAI
VMCAI 2020VMCAI 2020
Acta Informatica
ATVA
ATVA 2019, International Symposium on Automated Technology for Verification and Analysis
OPODIS
22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China
Formal Methods for Finding and Fixing Information Leaks
Information leaks are a security topic that makes it to the news regularly, with side-channel attacks like Spectre showing how vulnerable much of our information infrastructure is. Systems that store and manipulate sensitive data should be secured against information leaks, but attackers keep finding more sophisticated attacks on systems that have been deemed secure thus far, exploiting side-channels and low-level behavior of the system hardware. Due to the abundance of possible leaks, it is almost impossible for a human designer to prevent them, and automatic formal methods can play a crucial role in finding and fixing such leaks.
In this seminar, students will learn to present, discuss, and summarize papers that aim at formalizing, analyzing and automatically fixing information leaks. The seminar is split into two parts. The first part will take the form of reading sessions, where we lay the foundations of the topic. For the second part, each student is assigned a recent paper from the research area. Students will present their paper and will write a seminar paper on the topic assigned to them, taking into account connections to the topics discussed in the seminar.
First Meeting: tba.
During our first meeting, I will present a short overview of the content and format of the seminar.
Reading Group: In the reading group sessions, we discuss background papers that lay the foundations, or give an overview of the recent work on formal methods for security. Each paper will be presented informally by selected students, followed by a joint discussion. The list of papers for the reading group will be announced soon.
Talks: At the first reading group session, each participant will be assigned a topic. Each topic will be presented by the respective student, followed by joint discussion. For the discussions, it is important that every participant has read the paper(s) that are presented. The list of presentation topics will be announced soon.
Summary: At the end of the seminar we would like you to submit a summary of the seminar topics, including a comparison of your topic to the ones presented by other students.
Parameterized Verification
| Lecture Room: | tba. |
| Lectures: | tba. |
| Tutorials: | tba. |
| Exams: | tba. |
We consider the problem of providing correctness and security guarantees for systems that scale with some parameter, e.g., the number of nodes in a network, the number of concurrent processes in a multi-threaded program, or the size of a data structure that a program operates on. Most systems are expected to scale in one or several parameters, but correctness and security guarantees are usually only given for fixed parameter values. In contrast, parameterized verification is the problem of obtaining correctness guarantees for all parameter values. In this course, we will look at methods for parameterized verification and investigate their capabilities and limitations.
The course is aimed at students interested in the theoretical concepts behind parameterized verification, which generalize system models, specification formalisms and proof methods from standard verification approaches. The course picks up on some of the topics of the core lecture "Verification", which is highly recommended, but not a prerequisite for this course.
The course will be loosely based on the following textbook, supplemented by recent research results in the area:
Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
Morgan&Claypool, Synthesis Lectures on Distributed Computing Theory (2015)
(hardcopies should be available in the library, a PDF is available through CMS)
Advanced Lecture: Reactive Synthesis
This course is aimed at students that are interested in reactive synthesis in its full breadth, ranging from its theoretical formalization as an infinite game to efficient algorithms and data structures to solve the synthesis problem, and in the implementation of state-of-the-art algorithms for practically relevant and challenging problems.
Seminar: Formal Methods for Security
Engineering of secure systems is an arms race between attackers and system designers. In recent years, hardly a week goes by without the discovery of a new attack, and system designers scrambling to plug the holes. Formal methods are a means to break out of this arms race by ruling out entire classes of attacks once and for all.