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 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)

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.

2021
DOI [bibtex]
@article{C2021,
title = {Counterexample-guided inductive synthesis for probabilistic systems},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal aspects of computing},
pages = {31 Seiten},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00165-021-00547-2},
url = { https://publications.rwth-aachen.de/record/820111},
}×
[issue]
Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems, Formal aspects of computing, 31 Seiten, Springer, 2021.
2020
DOI fulltext PDF [bibtex]
@phdthesis{PM2020,
title = {Parameter synthesis in Markov models},
author = {Sebastian Junges},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource (xv, 371 Seiten) : Illustrationen},
type = {PhD Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-02348},
url = { https://publications.rwth-aachen.de/record/783179},
}×
[issue]
Sebastian Junges. Parameter synthesis in Markov models, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xv, 371 Seiten) : Illustrationen, 2020.
DOI fulltext PDF [bibtex]
@conference{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32nd International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020.
fulltext PDF [bibtex]
@techreport{URTGURAVL2020,
title = {UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic},
author = {Joost-Pieter Katoen and Martin Ritzert and Richard Wilke and Katrin M. Dannert and Peter Lindner and Dennis Fischer and Janosch Fuchs and Björn Frederik Tauer and Vipin Ravindran Vijayalakshmi and Laura Vargas Koch and Nadine Friesen and Andreas Gabriel Klinger and Marcel Tobias Hark and Benjamin Lucien Kaminski and Sebastian Junges and Jip Josephine Spel and Anton Pirogov and Stefan Schupp and Till Hofmann and Daxin Liu and Martin Comis and Tabea Claudia Krabs and Stephan Zieger and Rebecca Haehn and Matthias Volk and Norman Weik and Helene-Maria Bolke-Hermanns},
pages = {85 Seiten},
type = {Tech Report},
year = {2020},
url = { https://publications.rwth-aachen.de/record/807487},
}×
[issue]
Joost-Pieter Katoen, Martin Ritzert, Richard Wilke, Katrin M. Dannert, Peter Lindner, Dennis Fischer, Janosch Fuchs, Björn Frederik Tauer, Vipin Ravindran Vijayalakshmi, Laura Vargas Koch, Nadine Friesen, Andreas Gabriel Klinger, Marcel Tobias Hark, Benjamin Lucien Kaminski, Sebastian Junges, Jip Josephine Spel, Anton Pirogov, Stefan Schupp, Till Hofmann, Daxin Liu, Martin Comis, Tabea Claudia Krabs, Stephan Zieger, Rebecca Haehn, Matthias Volk, Norman Weik, Helene-Maria Bolke-Hermanns. UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic, 85 Seiten, 2020.
DOI fulltext PDF [bibtex]
@article{MBTAM2020,
title = {Multi-cost Bounded Tradeoff Analysis in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
journal = {Journal of automated reasoning},
volume = {64(7)},
pages = {pages 1483-1522},
type = {Journal Article},
year = {2020},
doi = {10.1007/s10817-020-09574-9},
url = { https://publications.rwth-aachen.de/record/794977},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, Journal of automated reasoning 64 (7), pages 1483-1522, Springer, 2020.
DOI [bibtex]
@conference{SBVUM2020,
title = {Scenario-Based Verification of Uncertain MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12078},
pages = {287-305},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_16},
url = { https://publications.rwth-aachen.de/record/794207},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Scenario-Based Verification of Uncertain MDPs, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 12078 of Theoretical Computer Science and General Issues, 287-305, Springer, 2020.
DOI [bibtex]
@article{PMPG2020,
title = {Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination},
author = {Christel Baier and Christian Hensel and Lisa Hutschenreiter and Sebastian Junges and Joost-Pieter Katoen and Joachim Klein},
publisher = {Elsevier},
journal = {Information and computation},
volume = {272},
pages = {pages 104504},
type = {Journal Article},
year = {2020},
doi = {10.1016/j.ic.2019.104504},
url = { https://publications.rwth-aachen.de/record/793292},
}×
[issue]
Christel Baier, Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein. Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Information and computation 272, pages 104504, Elsevier, 2020.
arXiv:2004.14835 [bibtex]
@unpublished{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
type = {Preprint},
year = {2020},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835
Show all