Swen Jacobs
Contact
Swen Jacobs
CISPA Helmholtz Center for Information Security
Saarland Informatics Campus
Phone: +49 681 302 5666
eMail: jacobs@cispa.saarland
Office: Building E 1.1, room 1.13
About me
I am a faculty member at the CISPA Helmholtz Center for Information Security.
I am looking for motivated and talented students, and have open PhD positions.
If you would like to work with me, email me with a statement explaining your interest in my research.
Teaching
- Advanced Lecture: Reactive Synthesis, Winter 2019/20 (block course), Saarland University
- Seminar: Formal Methods for Security (Register), Winter 2019/20, Saarland University
- Advanced Lecture: Parameterized Verification, Summer 2019, Saarland University
- Seminar: Selected Topics in Formal Methods for Security, Winter 2018/19, Saarland University
- Core Lecture: Embedded Systems, Summer 2018, Saarland University
- Proseminar: Formal Verification of Security Protocols, Summer 2018, Saarland University
- Advanced Lecture: Reactive Synthesis, Winter 2017/18, Saarland University
Selected Talks
- Reliable Security Guarantees. CISPA Young Researcher Security Convention, Apr 2019.
- Parameterized Verification and Synthesis. Scientific Colloquium in the Habilitation Process, Saarland University, Feb 2019.
My Research
My research mission is to make it easier to obtain systems with reliable correctness guarantees.
To this end, I am developing methods and tools for the rigorous analysis and design of software and hardware, based on formal verification and automatic synthesis.
Application domains include concurrent and distributed systems, security-critical software and hardware, and any kind of system that is expected to scale with the number of users or participants.Events
Organizer/OC member:
- ACM CCS 2019 (26th Conference on Computer and Communications Security, Web Chair)
- FRIDA 2019 (6th Workshop on Formal Reasoning in Distributed Algorithms, Co-organizer)
- SYNTCOMP 2019 (Reactive Synthesis Competition, Co-organizer), annually since 2014
PC member:
- SYNT 2019 (8th Workshop on Synthesis)
- PPoPP 2019 (24th ACM SIGPLAN Annual Symposium on Principles and Practice of Parallel Programming, Extended Review Committee)
- CAV 2018 (30th International Conference on Computer Aided Verification, Artifact Evaluation Committee)
- VSTTE 2018 (10th Working Conference on Verified Software: Theories, Tools, and Experiments)
Selected Publications
(Also find publication lists at Google Scholar and DBLP)
2019
- A symbolic algorithm for lazy synthesis of eager strategies (with M. Sakr)
in Acta Informatica, to appear.
- Efficient Information-Flow Verification under Speculative Execution (with R. Bloem and Y. Vizel)
in ATVA 2019, to appear.
- The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
(with R. Bloem, M. Colange, P. Faymonville, B. Finkbeiner, A. Khalimov, F. Klein, M. Luttenberger, P. J. Meyer, T. Michaud, M. Sakr, S. Sickert, L. Tentrup, A. Walker)
arXiv preprint, 2019.
2018
- Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings (with N. Mirzaie, F. Faghih and B. Bonakdarpour)
in OPODIS 2018, LIPIcs 125, 2018, pages 29:1-29:17.
- Design Understanding: From Logic to Specification
(with G. Fey, T. Ghasempouri, G. Martino, J. Raik and H. Riener)
in VLSI-SoC 2018, IEEE, 2018, pages 172-175. (pdf)
- A Symbolic Algorithm for Lazy Synthesis of Eager Strategies (with M. Sakr)
in ATVA 2018, LNCS 11138, 2018, pages 211-227.
- Distributed Synthesis for Parameterized Temporal Logics (with L. Tentrup and M. Zimmermann)
in Information & Computation 262(2), 2018, pages 311-328.
- Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity (with M. Sakr)
in VMCAI 2018, LNCS 10747, 2018, pages 247-268.
2017
- Proceedings of the Sixth Workshop on Synthesis (with D. Fisman, editors). EPTCS 260, 2017.
- The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results
(with N. Basset, R. Bloem, R. Brenguier, M. Colange, P. Faymonville, B. Finkbeiner, A. Khalimov, F. Klein, T. Michaud, G. A. Pérez, J.-F. Raskin, O. Sankur, L. Tentrup)
in SYNT 2017, EPTCS 260, 2017, pages 116-143.
- The First Reactive Synthesis Competition (SYNTCOMP 2014)
(with R. Bloem, R. Brenguier, R. Ehlers, T. Hell, R. Könighofer, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in STTT 19(3), 2017, pages 367-390.
2016
- The Third Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants and Results
(with R. Bloem, R. Brenguier, A. Khalimov, F. Klein, R. Könighofer, J. Kreber, A. Legg, N. Narodytska, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in SYNT 2016, EPTCS 229, 2016, pages 149-177.
- The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond (with R. Bloem)
in SYNT 2016, EPTCS 229, 2016, pages 133-148.
- A High-Level LTL Synthesis Format: TLSF v1.1 (with F. Klein and S. Schirmer)
in SYNT 2016, EPTCS 229, 2016, pages 112-132.
- Distributed PROMPT-LTL Synthesis (with L. Tentrup and M. Zimmermann)
in GandALF 2016, EPTCS 226, 2016, pages 228-241.
- Synthesis of Self-Stabilizing and Byzantine-Resilient Distributed Systems (with R. Bloem and N. Braud-Santoni)
in CAV 2016, LNCS 9779, pages 157-176.
- Decidability in Parameterized Verification
(with R. Bloem, A. Khalimov, I. Konnov, S. Rubin, H. Veith and J. Widder)
in ACM SIGACT News 47(2), 2016, pages 53-64.
- Tight Cutoffs for Guarded Protocols with Fairness (with S. Außerlechner and A. Khalimov)
in VMCAI 2016, LNCS 9583, pages 476-494. Full version on arXiv.
2015
- The Second Reactive Synthesis Competition (SYNTCOMP 2015)
(with R. Bloem, R. Brenguier, R. Könighofer, G. A. Pérez, J.-F. Raskin, L. Ryzhyk, O. Sankur, M. Seidl, L. Tentrup and A. Walker)
in SYNT 2015, EPTCS 202, pages 27-57.
- Decidability of Parameterized Verification
(with R. Bloem, A. Khalimov, I. Konnov, S. Rubin, H. Veith and J. Widder)
in series: Synthesis Lectures in Distributed Computing Theory, Morgan & Claypool.
- Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
(with R. Bloem, K.Chatterjee and R. Koenighofer)
in TACAS 2015, LNCS 9035, pages 517-532.
Full version on arXiv.
2014
- Parameterized Synthesis Case Study: AMBA AHB (with R. Bloem and A. Khalimov)
in SYNT 2014, EPTCS 157, pages 68-83.
- How to Handle Assumptions in Synthesis (with R. Bloem, R. Ehlers and R. Könighofer)
in SYNT 2014, EPTCS 157, pages 34-50.
- Parameterized Synthesis (with R. Bloem)
in LMCS 10(1:12), pages 1-29.
- Parameterized Model Checking of Token-Passing Systems
(with B. Aminof, A. Khalimov and S. Rubin)
in VMCAI 2014, LNCS 8318, pages 262-281.
2013
- PARTY Parameterized Synthesis of Token Rings (with A. Khalimov and R. Bloem)
in CAV 2013, LNCS 8044, pages 928-933.
- Towards Efficient Parameterized Synthesis (with A. Khalimov and R. Bloem)
in VMCAI 2013, LNCS 7737, pages 108-127.
- Reductions for Synthesis Procedures (with V. Kuncak and P. Suter)
in VMCAI 2013, LNCS 7737, pages 88-107.
2012
- Parameterized Synthesis (with R. Bloem)
in TACAS 2012, LNCS 7214, pages 362-376.
- Lazy Synthesis (with B. Finkbeiner)
in VMCAI 2012, LNCS 7148, pages 219-234.
-2011
- Towards Complete Reasoning about Axiomatic Specifications (with V. Kuncak)
in VMCAI 2011, LNCS 6538, pages 278-293, 2011. Extended Version as EPFL Technical Report, 2010.
- Automatic Verification of Parametric Specifications with Complex Topologies
(with J. Faber, C. Ihlemann and V. Sofronie-Stokkermans)
in IFM 2010, LNCS 6396, pages 152-167, 2010. Extended Version as AVACS Technical Report, 2010.
- Hierarchic Decision Procedures for Verification
PhD Thesis, Saarland University, 2010. Thesis advisor: Viorica Sofronie-Stokkermans
- Incremental Instance Generation in Local Reasoning
in CAV 2009, LNCS 5643, pages 368-382, 2009.
- On Local Reasoning in Verification (with C. Ihlemann and V. Sofronie-Stokkermans)
in TACAS 2008, LNCS 4963, pages 265-281, 2008.
- Exact State Set Representation in the Verification of Linear Hybrid Systems with Large Discrete State Space
(with W. Damm, S. Disch, H. Hungar, J. Pang, F. Pigorsch, C. Scholl, U. Waldmann and B. Wirtz)
in ATVA 2007, LNCS 4762, pages 425-440, 2007.
- Verifying CSP-OZ-DC specifications with complex data types and timing parameters
(with J. Faber and V. Sofronie-Stokkermans)
in IFM 2007, LNCS 4591, pages 233-252, 2007.
- Applications of Hierarchical Reasoning in the Verification of Complex Systems
(with V. Sofronie-Stokkermans)
in ENTCS 174/8 (Special issue dedicated to PDPAR’06), pages 39-54, 2007.
- Comparing Instance Generation Methods for Automated Reasoning (with U. Waldmann)
in JAR 38, pages 57-78, 2007.