Sebastian Junges

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?

Research Interest

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.

Tool support

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:



Invited Talks

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:

Older topics include:

Professional Activities

PC Membership

Editorial Boards

External Reviewer


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.

Organised Events

Event participation


Thesis supervision

Lectures (Teaching Assistance)

Guest lectures

Seminar Projects

Lab supervision

Student team

I was team-leader in the CaroloCup, where a student team rebuilds an RC-Car in scale 1:10 to an autonomous vehicle.