Sebastian Junges


sebastian.junges at
Room 4210
Ahornstra├če 55
D-52074 Aachen
+49 241 80 21203

I have been a PhD student at the Software Modeling and Verification Group since June 2015. Since October 2017, I have been affiliated with the Research Training Group UnRAVeL.

You can also find me on DBLP and Google Scholar.

Research interests

  • Model checking of quantitative (parameterised) systems
  • Policy synthesis for variants of partially observable MDPs
  • Formal aspects of reliability engineering, in particular fault trees
  • SMT-solving for real arithmetic
  • Formal modelling of real-world systems

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:

  • The SMT-solver SMT-RAT (2011 — 2015)
  • The arithmetic library carl (2012 — 2015) and its python bindings pycarl (since 2016)
  • Compass (2014)
  • The Markov Chain Parameter Synthesis Framework PROPhESY (since 2014)
  • The Probabilistic Model Checker Storm (since 2014) and its python bindings stormpy (since 2016)

B.Sc or M.Sc theses

I’m always looking forward to work with students. If you’re looking for a thesis in one of the areas above, do not hesitate to contact me! Some ideas are given in our list of open topics.

Previously, I supervised the following theses (chronological order):

  • Tom Janson, Accelerated Model Repair using Heuristic Analysis of Subsystems (BSc)
  • Tim QuatmannMulti-Objective Model Checking for Markov Automata (MSc)
  • Ronja Nocon, Pattern-based detection of Monotonicity in Dynamic Fault Trees (BSc) [together with Matthias Volk]
  • Michael Deutschen, GSPN Semantics for Dynamic Fault Trees (MSc) [together with Matthias Volk]
  • Dustin Jungen, Repairs in Dynamic Fault Trees (BSc) [together with Matthias Volk]
  • Sebastian Kruse, Model Checking a Wireless Token-Passing Network (MSc)
  • Sven Deserno,  Model Checking Families of Markov Chains (MSc) [together with Benjamin Kaminski]
  • Jip SpelMonotonicity in Markov Chains (MSc)


I was involved in teaching assistance for the following lectures:

Furthermore, I supervised students in the scope of the following seminars:


I have been PC Member for the Artefact Evaluation of ATVA. 

I have been an external reviewer for the following venues:

and for the following journals:
FMSD, J.Systems and Software.

Publications for Sebastian Junges

Milan Ceska, Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches. Proc. of FM, , 2019.
Tobias Winkler, Sebastian Junges, Guillermo A Perez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. Proc. of CONCUR, , 2019.
DOILinkMajdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees. Reliability Engineering and System Safety 186, pages 37–50, 2019.
Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains. Proc. of TACAS, Volume of LNCS, , 2019.
Show all


External Talks

Show all