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.
DOIMurat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. Proc. of ATVA, Volume 11138 of LNCS, pages 160-176, Springer, 2018.
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking For Safe Navigation Among Humans. Proc. of QEST, Volume of LNCS, , 2018.
LinkSebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs via Parameter Synthesis. Proc. of UAI, AUAI, 2018.
DOILinkSebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A unifying semantics of DFTs using GSPNs. Proc. of Petri Nets, Volume 10877 of LNCS, pages 272–293, Springer, 2018.
DOIArnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-Cost Bounded Reachability in MDPs. Proc. of TACAS, Volume 10805 of LNCS, , 2018.
DOIMatthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Transactions on Industrial Informatics 14(1), pages 370-379, 2018.
Show all


External Talks

Show all