Send email Copy Email Address

Short Bio

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.

CV: Last four stations

Since 2018
Faculty at CISPA Helmholtz Center for Information Security
2014 - 2018
Research group leader at Saarland University
2012 - 2014
Postdoctoral researcher at TU Graz
2012
Visiting professor at University of Ljubljana, Slovenia

Publications by Swen Jacobs

Year 2022

Conference / Medium

FMCAD
FMCAD 2022Formal Methods in Computer-Aided Design 2022

Year 2021

Conference / Medium

CAV
Computer Aided Verification - 33nd International Conference, CAV 202133rd International Conference on Computer-Aided Verification

Year 2020

Conference / Medium

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

Year 2019

Conference / Medium

ATVA
ATVA 2019, International Symposium on Automated Technology for Verification and Analysis

Year 2018

Conference / Medium

OPODIS
22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China

Teaching by Swen Jacobs

Winter 2021/22

Formal Methods for Finding and Fixing Information Leaks

Seminar Topic

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.

Important Dates

First Meeting: tba.

During our first meeting, I will present a short overview of the content and format of the seminar.

Requirements

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.

Winter 2021/22

Parameterized Verification

Advanced Lecture (Vertiefungsvorlesung), Winter Term 2021/22, 6 CP

Lecture Room: tba.
Lectures: tba.
Tutorials: tba.
Exams: tba.
   

Topic

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.

References

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)

Winter 2019/20

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.

Winter 2019/20

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.