Email

sebastian.junges at cs.rwth-aachen.de

Address

Room 4210
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21203

I have been a PhD student at the Software Modeling and Verification Group since June 2015. Since October 2017, I have been 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
• 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]

Teaching

I am currently involved in teaching assistance for:

• Concurrency Theory (Winter 2017)

I was involved in teaching assistance for the following lectures:

• 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:

• Programming Language Design and Implementation (Seminar, Winter 2018)
• Introduction to Program Analysis (Proseminar, Winter 2016)
• Probabilistic Programming (Seminar, Summer 2016)
• Algorithms and Data Structures (Proseminar, Winter 2015)

Reviewer

I have been an external reviewer for the following venues: MMB’16, CAV’16, ICALP’16, FM’16, HVC’16, PSI’17, SafeComp’17, ATVA’17, Gandalf’17, ADHS’18, FM’18, FORTE’18, and for the following journals: FMSD, J.Systems and Software

Publications for Sebastian Junges

2018
	Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A unifying semantics of DFTs using GSPNs. Proc. of Petri Nets, Volume of LNCS, Springer, 2018.
	Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-Cost Bounded Reachability in MDPs. Proc. of TACAS, Volume 10805 of LNCS, , 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, 2018.
2017
	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.
	Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems. Proc. of SAFECOMP, Volume 10488 of LNCS, pages 3–19, Springer, 2017.
	Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. Proc. of CAV, Volume 10427 of LNCS, pages 592–600, Springer, 2017.
	Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives. Proc. of Computer Aided Verification (CAV), Volume 10426 of LNCS, pages 140–159, Springer, 2017.
	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. Proc. of TACAS, Volume 10206 of LNCS, pages 133-150, Springer, 2017.
	Carlos E. Budde, Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. “JANI: Quantitative Model and Tool Interaction. Proc. of TACAS (2), Volume 10206 of LNCS, pages 151-168, Springer, 2017.
	Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Marielle Stoelinga. Fault Trees on a Diet: Automated Reduction by Graph Rewriting. Formal Aspects of Computing 29(4), pages 651-703, 2017.
Show all

 

External Talks

2017
	Sebastian Junges. Recent Advances in Dynamic Fault Tree Analysis, Talk at CAP Workshop, Heidelberg, Germany, 2017.
	Sebastian Junges. Probabilistic Model Checking with Storm and Multi-Objective Markov Automata, Talk at IST, Klosterneuburg, Austria, 2017.
	Sebastian Junges. Safety and Dependability Analysis by Probabilistic Model Checking, Talk at Workshop on Safety at the Crossroads, Amsterdam, The Netherlands, 2017.
	Sebastian Junges. A Storm is Coming: A Modern Probabilistic Model Checker, Talk at ULB, Brussels, Belgium, 2017.
Show all