
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:
- Datastructures and Algorithms (Summer 2018)
- Concurrency Theory (Winter 2017)
- Compiler Construction (Summer 2017)
- Introduction to Model Checking (Summer 2016)
- Modeling and Verification of Probabilistic Systems (Winter 2015)
Furthermore, I supervised students in the scope of the following seminars:
- Introduction to Program Analysis (Proseminar, Sumer 2019)
- Trends and Pearls of Model Checking (Seminar, Winter 2019)
- Formal Verification Meets Machine Learning (Seminar, Summer 2018)
- Programming Language Design and Implementation (Seminar, Winter 2017)
- Introduction to Program Analysis (Proseminar, Winter 2016)
- Probabilistic Programming (Seminar, Summer 2016)
- Algorithms and Data Structures (Proseminar, Winter 2015)
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 | |
---|---|
![]() ![]() |
Kevin Batz, Mingshuai Chen, Sebastian Junges, , Joost-Pieter Katoen, . 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. |
![]() ![]() |
Roman Andriushchenko, Alexander Nikolai 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. |
![]() |
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 | |
![]() |
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. |
2021 | |
![]() |
Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems, Formal aspects of computing 33 (4/5), pages 637-667, Springer, 2021. | ,
2020 | |
![]() ![]() |
Sebastian Junges. Parameter synthesis in Markov models, PhD Thesis, RWTH Aachen University, 1 Online-Ressource (xv, 371 Seiten) : Illustrationen, 2020. |
![]() |
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835 |
![]() |
Hans Christian Hensel, , Sebastian Junges, Joost-Pieter Katoen, . Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Information and computation 272, pages 104504, Elsevier, 2020. | ,
![]() |
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, . Scenario-Based Verification of Uncertain MDPs, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 287-305, Springer, 2020. |
![]() ![]() |
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. |
![]() |
Joost-Pieter Katoen, Martin Ritzert, Richard Marlon 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. |
![]() ![]() |
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020. |
2019 | |
![]() |
Sebastian Junges, Joost-Pieter Katoen, , Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, Elsevier Science, 2019. | ,
![]() |
Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, , , . Correct-by-construction policies for POMDPs, 5. 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), ACM Digital Library, 6-8, ACM Press, 2019. | ,
![]() |
Hans Christian Dehnert, , Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019. | ,
![]() ![]() |
Tobias Winkler, Sebastian Junges, , Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, 30. International Conference on Concurrency Theory (CONCUR), Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019. |
![]() |
Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen. Are Parametric Markov Chains Monotonic?, 17. International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Volume 11781 of LNCS, 479-496, Springer, 2019. |
![]() ![]() |
Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 11428 of LNCS, 172-190, Springer, 2019. | , ,
![]() |
Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3. World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019. | ,
2018 | |
![]() |
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, IEEE, 2018. |
![]() ![]() |
Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Reachability in MDP, 24. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, 320-339, Springer, 2018. | ,
![]() |
Sebastian Junges, Joost-Pieter Katoen, , Matthias Volk. One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs, 39. International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, 272-293, Springer, 2018. |
![]() |
Sebastian Junges, Joost-Pieter Katoen, . Synthesis in pMDPs: A Tale of 1001 Parameters, 16. International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Volume 11138 of LNCS, 160-176, Springer, 2018. | , ,
![]() |
Sebastian Junges, , Joost-Pieter Katoen, , , . Model Checking for Safe Navigation Among Humans, 15. International Conference on Quantitative Evaluation of Systems (QEST 2018), Volume 11024, Theoretical Computer Science and General Issues of LNCS, 207-222, Springer, 2018. |
![]() |
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, , Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, AUAI Press, 2018. |
[bibtex] [issue] | Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, , Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, Curran Associates, Inc., 2018. |
2017 | |
![]() |
Sebastian Junges, , Joost-Pieter Katoen, , . Fault trees on a diet: automated reduction by graph rewriting, Formal aspects of computing 29 (4), pages 651-703, Springer, 2017. |
![]() |
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311 |
![]() |
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017. |
![]() |
Sebastian Junges, Joost-Pieter Katoen, , , . Sequential Convex Programming for the Efficient Verification of Parametric MDPs, 23. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 133-150, Springer, 2017. | , ,
![]() |
Hans Christian Dehnert, , , Sebastian Junges, . JANI: Quantitative Model and Tool Interaction, 23. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 151-168, Springer, 2017. | ,
![]() |
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, 140-159, Springer, 2017. |
![]() |
Sebastian Junges, Joost-Pieter Katoen, , Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, 36. International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, 3-19, Springer, 2017. | ,
![]() |
Sebastian Junges, , , , Joost-Pieter Katoen, . Motion planning under partial observability using game-based abstraction, IEEE 56. Annual Conference on Decision and Control (CDC), 2201-2208, IEEE, 2017. | ,
2016 | |
![]() |
Tim Quatmann, Hans Christian Dehnert, , Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016. |
![]() ![]() |
Hans 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), 72-74, Albert-Ludwigs-Universität, 2016. |
![]() |
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, . Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks, IEEE 35. Symposium on Reliable Distributed Systems (SRDS 2016), 307-316, IEEE, 2016. |
![]() |
Sebastian Junges, Nils Jansen, Hans Christian Dehnert, , Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs, 22. international conference, held as part of the European Joint Conferences on Theory and Practice of Software (TACAS 2016), Volume 9636 of LNCS, 130-146, Springer, 2016. |
![]() |
Sebastian Junges, , Joost-Pieter Katoen, . Uncovering Dynamic Fault Trees, 46. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2016), 299-310, IEEE, 2016. |
![]() |
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, 35. International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Volume 9922 of LNCS, 253-265, Springer, 2016. |
![]() |
Sebastian Junges, , Joost-Pieter Katoen, . Probabilistic Verification for Cognitive Models, AAAI 2016 Fall Symposium, Volume FS-16-03 of AAAI Technical Reports, 185-188, AAAI Press, 2016. |
2015 | |
![]() |
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, 360-368, Springer, 2015. |
![]() |
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, 214-231, Springer, 2015. |
![]() |
Sebastian Junges, , Joost-Pieter Katoen, , . Fault Trees on a Diet, 1. International Symposium on Dependable Software Engineering (SETTA 2015), Volume 9409 of LNCS, 3-18, Springer, 2015. |
2014 | |
![]() |
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, 177-192, Springer, 2014. |
2013 | |
![]() |
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 : 5. international conference (CAI 2013), Volume 8080 of LNCS, 186-198, Springer, 2013. |
![]() |
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, 3-21, Shaker [u.a.], 2013. |