This website is under construction
I am a researcher and have been a PostDoc at UC Berkeley since March 2020. I am part of the Learn and Verify Group, headed by Sanjit Seshia.
Previously, I was a PhD student at RWTH Aachen University, under the supervision of Joost-Pieter Katoen.
I defended my PhD thesis titled Parameter Synthesis in Markov Models (pdf) in February 2020.
You can reach me at sjunges?berkeley.edu.
I am broadly interested in the automatic analysis of critical systems.
This interest includes both modelling and verification aspects.
In particular, I am interested in the analysis of models that explicitly model uncertainty.
I often work with probabilstic model checkers and SAT/SMT solvers and analyze extensions of Markov decision processes (MDPs),
in particular also parametric or partially observable MDPs. My research is largely driven by the development and implementation of algorithms.
For now, please refer to DBLP or Google Scholar for an overview of my publications.
Over the years, I’ve been involved in the development of the following tools to advance the state-of-the-art in computer aided verification:
- The probabilistic model checker Storm (since 2014) and its python bindings stormpy (since 2016)
- The parameter synthesis framework for Markov models PROPhESY (since 2014)
- The SMT-solver SMT-RAT (2011 — 2015)
- The arithmetic library carl (2012 — 2015) and its python bindings pycarl (since 2016)
- Compass (2014)
- Borchers Plakette 2020, ProRWTH, for finishing my PhD with distinction.
- RWTH ICT Young Researcher Award 2017, for advancing the state-of-the-art in a subfield of ICT.
- Fakultätentag Informatik Preis 2015, awarded for the best CS-related Master Thesis at a German University.
- Master Preis der Fachgruppe Informatik (RWTH Aachen Univeristy CS Department) for results during my studies.
- Springorum-Denkmuenze 2015, ProRWTH, for finishing my studies with distinction.
I have given invited talks at:
Moreover, I have given (external) seminar talks at ISCAS (Beijing), IST Austria, LaBRI (Bordeaux), Stanford, UC Berkeley, ULB (Brussels), and at the ROCKS Meetings.
I have recently given talks about:
- The Computational Complexity of Finding Memoryless Policies in POMDPs
- A SAT-based approach to Enforcing Almost-Sure Reachability in POMDPs
- Advanced Methods for the Quantitative Analysis of Software Product Lines
- The Probabilistic Model Checker Storm
- Parameter Synthesis for Markov Models
Older topics include:
- Modelling and Analysis with Dynamic Fault Trees
- Multi-objective Model Checking of Markov Automata
ATVA, ADHS, CAV, CDC, Concur, FM, FSEN, FORTE, Gandalf, HVC, ICALP, iFM, Memocode, MMB, PSI, QEST, SafeComp, TACAS
FMSD, J. Intelligent Robot Syst, J.Systems and Software, JCST, Machine Learning, STTT.
- I co-organised the 1st and 2nd UnRAVEL Spring Meetings.
- I co-organised the ‘Aachener Informatik Tage’, a STEM-outreach event for highschool pupils, several times.
- Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc, RWTH)
- Tim Quatmann, Multi-Objective Model Checking for Markov Automata (MSc, RWTH)
- Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
- Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc, RWTH) – together with Matthias Volk
- Dustin Jungen, Repairs in Dynamic Fault Trees (BSc, RWTH) – together with Matthias Volk
- Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc, RWTH)
- Sven Deserno, Model Checking Families of Markov Chains (MSc, RWTH) – together with Benjamin Kaminski
- Jip Spel, Monotonicity in Markov Chains (MSc, University of Twente)
- Dustin Jungen, SAT-Based Methods for Solving POMDP problems (MSc, RWTH)
- Kevin Batz, Probabilistic IC3 (MSc, RWTH) – together with Benjamin Kaminski and Christoph Matheja
- Marnix Suilen, Multi-environment MDPs – with Nils Jansen
Lectures (Teaching Assistance)
- Model Checking (RWTH, Winter 2019)
- Datastructures and Algorithms (RWTH, Summer 2018)
- Concurrency Theory (RWTH, Winter 2017)
- Compiler Construction (RWTH, Summer 2017)
- Introduction to Model Checking (RWTH, Summer 2016)
- Modeling and Verification of Probabilistic Systems (RWTH, Winter 2015)
- Introduction to probabilistic model checking (UC Berkeley, Formal Methods, 2020)
- On parameter synthesis (RWTH, Modeling and Verification of Probabilistic Systems, 2019)
- Introduction to Program Analysis (RWTH, Proseminar, Sumer 2019)
- Trends and Pearls of Model Checking (RWTH, Seminar, Winter 2019)
- Formal Verification Meets Machine Learning (RWTH, Seminar, Summer 2018)
- Programming Language Design and Implementation (RWTH, Seminar, Winter 2017)
- Introduction to Program Analysis (RWTH, Proseminar, Winter 2016)
- Probabilistic Programming (RWTH, Seminar, Summer 2016)
- Algorithms and Data Structures (RWTH, Proseminar, Winter 2015)
- Multi-agent systems with Lego Mindstorms (Winter 2013)
I was team-leader in the CaroloCup, where a student team rebuilds an RC-Car in scale 1:10 to an autonomous vehicle.