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.

2020
DOI fulltext PDF [bibtex] [issue] Arnd Hartmanns, Joost-Pieter Katoen, Sebastian Junges, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, Journal of automated reasoning 64 (7), pages 1483-1522, Springer, 2020.
DOI fulltext PDF [bibtex] [issue] Sebastian Junges. Parameter synthesis in Markov models, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xv, 371 Seiten) : Illustrationen, 2020.
DOI [bibtex] [issue] Joost-Pieter Katoen, Murat Cubuktepe, Nils Jansen, Sebastian Junges, 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] [issue] Christel Baier, Christian Hensel, Joachim Klein, Joost-Pieter Katoen, Lisa Hutschenreiter, Sebastian Junges. Parametric Markov chains, Information and computation 272, pages 104504, Elsevier, 2020.
2019
DOI [bibtex] [issue] Joost-Pieter Katoen, Majdi Ghadhab, Matthias Kuntz, Matthias Volk, Sebastian Junges. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, Elsevier Science, 2019.
DOI [bibtex] [issue] Bernd Becker, Joost-Pieter Katoen, Leonore Winterer, Nils Jansen, Ralf Wimmer, Sebastian Junges, Tim Quatmann. Correct-by-construction policies for POMDPs, 5th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR) held as part of the 12th Cyber-Physical Systems and Internet-of-Things Week (CPS-IoT Week) (SNR '19), 6-8, ACM Press, 2019.
DOI [bibtex] [issue] Christian Dehnert, Joost-Pieter Katoen, Milan Češka, Nils Jansen, Sebastian Junges. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019.
DOI fulltext PDF [bibtex] [issue] Guillermo A. Pérez, Joost-Pieter Katoen, Sebastian Junges, Tobias Winkler. On the Complexity of Reachability in Parametric Markov Decision Processes, CONCUR 2019, Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.
DOI [bibtex] [issue] Jip Josephine Spel, Joost-Pieter Katoen, Sebastian Junges. Are Parametric Markov Chains Monotonic?, 17th International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Volume 11781 of LNCS, 479-496, Springer, 2019.
DOI fulltext PDF [bibtex] [issue] Joost-Pieter Katoen, Milan Češka, Nils Jansen, Sebastian Junges. Shepherding Hordes of Markov Chains, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 11428 of LNCS, 172-190, Springer, 2019.
DOI [bibtex] [issue] Hans Christian Hensel, Joost-Pieter Katoen, Milan Češka, Sebastian Junges. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3rd World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019.
2018
[bibtex] [issue] Bernd Becker, Joost-Pieter Katoen, Leonore Winterer, Nils Jansen, Ralf Wimmer, Sebastian Junges, Tim Quatmann. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, Curran Associates, Inc., 2018.
fulltext PDF [bibtex] [issue] Bernd Becker, Joost-Pieter Katoen, Leonore Winterer, Nils Jansen, Ralf Wimmer, Sebastian Junges, Tim Quatmann. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, AUAI Press, 2018.
DOI [bibtex] [issue] Joost-Pieter Katoen, Matthias Volk, Sebastian Junges. Fast Dynamic Fault Tree Analysis by Model Checking Techniques, IEEE transactions on industrial informatics 14 (1), pages 370-379, IEEE, 2018.
DOI [bibtex] [issue] Joost-Pieter Katoen, Mary Hayhoe, Nils Jansen, Ruohan Zhang, Sebastian Junges, Ufuk Topcu. Model Checking for Safe Navigation Among Humans, 15th International Conference on Quantitative Evaluation of Systems (QEST), Volume 11024 of LNCS, 207-222, Springer, 2018.
DOI [bibtex] [issue] Joost-Pieter Katoen, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ufuk Topcu. Synthesis in pMDPs, 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Volume 11138 of LNCS, 160-176, Springer, 2018.
DOI [bibtex] [issue] Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk, Sebastian Junges. One Net Fits All, 39th International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, 272-293, Springer, 2018.
DOI fulltext PDF [bibtex] [issue] Arnd Hartmanns, Joost-Pieter Katoen, Sebastian Junges, Tim Quatmann. Multi-cost Bounded Reachability in MDP, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806 of LNCS, 320-339, Springer, 2018.
2017
DOI [bibtex] [issue] Bernd Becker, Joost-Pieter Katoen, Leonore Winterer, Nils Jansen, Ralf Wimmer, Sebastian Junges, Ufuk Topcu. Motion planning under partial observability using game-based abstraction, IEEE 56th Annual Conference on Decision and Control (CDC), 2201-2208, IEEE, 2017.
DOI [bibtex] [issue] Joost-Pieter Katoen, Sebastian Junges, Tim Quatmann. Markov Automata with Multiple Objectives, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, 140-159, Springer, 2017.
DOI [bibtex] [issue] Joost-Pieter Katoen, Majdi Ghadhab, Matthias Kuntz, Matthias Volk, Sebastian Junges. Model-based Safety Analysis for Vehicle Guidance Systems, 36th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, 3-19, Springer, 2017.
DOI [bibtex] [issue] Andrea Turrini, Arnd Hartmanns, Carlos E. Budde, E. Moritz Hahn, Hans Christian Dehnert, Sebastian Junges. JANI, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 151-168, Springer, 2017.
DOI [bibtex] [issue] Hasan A. Poonawala, Ivan Papusha, Joost-Pieter Katoen, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 133-150, Springer, 2017.
DOI [bibtex] [issue] Hans Christian Dehnert, Joost-Pieter Katoen, Matthias Volk, Sebastian Junges. A Storm is Coming, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
arXiv:1702.04311 [bibtex] [issue] Christian Dehnert, Joost-Pieter Katoen, Matthias Volk, Sebastian Junges. A storm is Coming, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311
DOI [bibtex] [issue] Arend Rensink, Dennis Guck, Joost-Pieter Katoen, Mariëlle Stoelinga, Sebastian Junges. Fault trees on a diet, Formal aspects of computing 29 (4), pages 651-703, Springer, 2017.
2016
DOI [bibtex] [issue] Christian Dombrowski, James Gross, Joost-Pieter Katoen, Sebastian Junges. Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks, 2016 IEEE 35th Symposium on Reliable Distributed Systems (SRDS) (SRDS 2016), 307-316, IEEE, 2016.
DOI [bibtex] [issue] Hans Christian Dehnert, Joost-Pieter Katoen, Nils Jansen, Sebastian Junges, Tim Quatmann. Parameter Synthesis for Markov Models, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
DOI fulltext PDF [bibtex] [issue] Christian Dehnert, Erika Ábrahám, Florian Corzilius, Harold Yorick Bruintjes, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Sebastian Junges. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI [bibtex] [issue] Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga, Sebastian Junges. Uncovering Dynamic Fault Trees, 299-310, IEEE, 2016.
DOI [bibtex] [issue] Hans Christian Dehnert, Joost-Pieter Katoen, Nils Jansen, Sebastian Junges, Ufuk Topcu. Safety-constrained Reinforcement Learning for MDPs, Volume 9636 of LNCS, 130-146, Springer, 2016.
DOI [bibtex] [issue] Joost-Pieter Katoen, Matthias Volk, Sebastian Junges. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, Volume 9922 of LNCS, 253-265, Springer, 2016.
fulltext PDF [bibtex] [issue] Joost-Pieter Katoen, Nils Jansen, Sebastian Junges, Ufuk Topcu. Probabilistic Verification for Cognitive Models, Volume FS-16-03 of AAAI Technical Reports, 185-188, AAAI Press, 2016.
2015
DOI [bibtex] [issue] Arend Rensink, Dennis Guck, Joost-Pieter Katoen, Mariëlle Stoelinga, Sebastian Junges. Fault Trees on a Diet, First International Symposium on Dependable Software Engineering (SETTA 2015), Volume 9409 of LNCS, 3-18, Springer, 2015.
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Hans Christian Dehnert, Harold Yorick Bruintjes, Joost-Pieter Katoen, Matthias Volk, Nils Jansen, Sebastian Junges. PROPhESY, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp. SMT-RAT, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, 360-368, Springer, 2015.
2014
DOI [bibtex] [issue] Dimitri Bohlender, Harold Yorick Bruintjes, Jens Katelaan, Sebastian Junges, Thomas Noll, Viet Yen Nguyen. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models, Volume 8803 of LNCS, 177-192, Springer, 2014.
2013
fulltext PDF [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Sebastian Junges, Ulrich Loup. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, 3-21, Shaker [u.a.], 2013.
DOI [bibtex] [issue] Erika Ábrahám, Florian Corzilius, Sebastian Junges, Ulrich Loup. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 8080 of LNCS, 186-198, Springer, 2013.