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] Sebastian Junges. Parameter synthesis in Markov models, PhD Thesis, RWTH Aachen University, 371 pages, 2020.
2019
DOI fulltext PDF [bibtex] Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. 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] Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer. 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), pages 6-8, ACM Press, 2019.
DOI restricted URL PDF [bibtex] Milan Češka, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, From Reactive Systems to Cyber-Physical Systems, Volume 11500 of LNCS, pages 107-125, Springer, 2019.
DOI [bibtex] Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, 2019.
2018
DOI [bibtex] Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs : A Tale of 1001 Parameters, 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Volume 11138 of LNCS, pages 160-176, Springer, 2018.
DOI [bibtex] Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking for Safe Navigation Among Humans, 15th International Conference on Quantitative Evaluation of Systems (QEST), Volume 11024 of LNCS, pages 207-222, Springer, 2018.
fulltext PDF [bibtex] Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34th Conference on Uncertainty in Artificial Intelligence (UAI 34), pages 519-529, AUAI Press, 2018.
DOI [bibtex] Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs, 39th International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, pages 272-293, Springer, 2018.
DOI fulltext PDF [bibtex] Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, 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, pages 320-339, Springer, 2018.
2017
DOI [bibtex] Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion planning under partial observability using game-based abstraction, IEEE 56th Annual Conference on Decision and Control (CDC), pages 2201-2208, IEEE, 2017.
DOI [bibtex] Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, 36th International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, pages 3-19, Springer, 2017.
DOI [bibtex] Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, pages 140-159, Springer, 2017.
DOI [bibtex] Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, pages 592-600, Springer, 2017.
DOI [bibtex] Carlos E. Budde, Hans Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. JANI: Quantitative Model and Tool Interaction, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, pages 151-168, Springer, 2017.
DOI [bibtex] Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, 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, pages 133-150, Springer, 2017.
2018
DOI [bibtex] Matthias 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.
2017
arXiv:1702.04311 [bibtex] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 2017. arXiv:1702.04311
DOI [bibtex] Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault trees on a diet: automated reduction by graph rewriting, Formal aspects of computing 29 (4), pages 651-703, 2017.
2016
fulltext PDF [bibtex] Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models, AAAI 2016 Fall Symposium, Volume FS-16-03 of AAAI Technical Reports, pages 185-188, AAAI Press, 2016.
DOI [bibtex] Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, pages 50-67, Springer, 2016.
DOI [bibtex] Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks, 2016 IEEE 35th Symposium on Reliable Distributed Systems (SRDS) (SRDS 2016), pages 307-316, IEEE, 2016.
DOI [bibtex] Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, 35th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Volume 9922 of LNCS, pages 253-265, Springer, 2016.
DOI [bibtex] Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees, 46th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2016), pages 299-310, IEEE, 2016.
DOI [bibtex] Sebastian Junges, Nils Jansen, Hans Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs, 22nd international conference, held as part of the European Joint Conferences on Theory and Practice of Software (TACAS 2016), Volume 9636 of LNCS, pages 130-146, Springer, 2016.
DOI fulltext PDF [bibtex] Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), pages 72-74, Albert-Ludwigs-Universität, 2016.
2015
DOI [bibtex] Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault Trees on a Diet, First International Symposium on Dependable Software Engineering (SETTA 2015), Volume 9409 of LNCS, pages 3-18, Springer, 2015.
DOI [bibtex] Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Ábrahám. SMT-RAT : an Open Source C++ Toolbox for Strategic and Parallel SMT Solving, International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Volume 9340 of LNCS, pages 360-368, Springer, 2015.
DOI [bibtex] Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY : A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214-231, Springer, 2015.
2014
DOI [bibtex] Dimitri Bohlender, Harold Yorick Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models, Leveraging applications of formal methods, verification and validation (ISoLA 2014), Volume 8803 of LNCS, pages 177-192, Springer, 2014.
2013
fulltext PDF [bibtex] Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Volume 2013,08 of Aachener Informatik-Berichte : AIB, pages 3-21, Shaker [u.a.], 2013.
DOI [bibtex] Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Ábrahám. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers, Algebraic informatics (CAI 2013), Volume 8080 of LNCS, pages 186-198, Springer, 2013.
2012
DOI [bibtex] Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Ábrahám. SMT-RAT : An SMT-Compliant Nonlinear Real Arithmetic Toolbox, Theory and applications of satisfiability testing, Volume 7317 of LNCS, pages 442-448, Springer, 2012.