Sebastian Junges

sjp_8106_01

This website is now outdated. Please visit my new website.

In February 2020, I defended my PhD Thesis titled ‘Parameter Synthesis in Markov Models’ with honours.

I was a PhD student at the Software Modeling and Verification Group between June 2015 and February 2020. From October 2017 until February 2020, I was 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 Quatmann, Multi-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 Spel, Monotonicity in Markov Chains (MSc)

Teaching

I was involved in teaching assistance for the following lectures:

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

Reviewer

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

I have been an external reviewer for the following venues:
ATVA, ADHS, CAV, CDC, FM, FORTE, Gandalf, ICALP, iFM, MMB, HVC, PSI, QEST, SafeComp,

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

2023
DOI fulltext PDF [bibtex]
@conference{PPVISII2023,
title = {Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants},
author = {Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {410-429},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_25},
url = { https://publications.rwth-aachen.de/record/957952},
}×
[issue] 		Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 410-429, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{SESPSP2023,
title = {Search and Explore: Symbiotic Policy Synthesis in POMDPs},
author = {Roman Andriushchenko and Alexander Bork and Milan Češka and Sebastian Junges and Joost-Pieter Katoen and Filip Macák},
publisher = {Springer},
booktitle = {LNCS},
volume = {13966},
pages = {113-135},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-37709-9_6},
url = { https://publications.rwth-aachen.de/record/968844},
}×
[issue] 		Roman Andriushchenko, Alexander Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák. Search and Explore: Symbiotic Policy Synthesis in POMDPs, 35. International Conference on Computer-Aided Verification (CAV 2023), Volume 13966 of LNCS, 113-135, Springer, 2023.
DOI [bibtex]
@conference{APGMMCA2023,
title = {A Practitioner’s Guide to MDP Model Checking Algorithms},
author = {Arnd Hartmanns and Sebastian Junges and Tim Quatmann and Maximilian Weininger},
publisher = {Springer},
booktitle = {LNCS},
volume = {13993},
pages = {469-488},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30823-9_24},
url = { https://publications.rwth-aachen.de/record/972074},
}×
[issue] 		Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13993 of LNCS, 469-488, Springer, 2023.
2022
DOI [bibtex]
@article{COPSM2022,
title = {Convex Optimization for Parameter Synthesis in MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Institute of Electrical and Electronics Engineers},
journal = {IEEE transactions on automatic control},
volume = {67(12)},
pages = {pages 6333-6348},
type = {Journal Article},
year = {2022},
doi = {10.1109/TAC.2021.3133265},
url = { https://publications.rwth-aachen.de/record/888868},
}×
[issue] 		Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Convex Optimization for Parameter Synthesis in MDPs, IEEE transactions on automatic control 67 (12), pages 6333-6348, Institute of Electrical and Electronics Engineers, 2022.
Show all