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.

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

Research in automated verification is impossible without proper tool support.  Over the years, I’ve been involved in the development of

• 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 Quatman, 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]

Teaching

I am currently involved in teaching assistance for 

• Compiler Construction (Summer 2017)

I was involved in teaching assistance for the following lectures:

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

Publications for Sebastian Junges

2017
	Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Transactions on Industrial Informatics, 2017.
	Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems. Proc. of SAFECOMP, Volume of LNCS, , 2017.
	Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. Proc. of CAV, , 2017.
	Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives. Proc. of CAV, , 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 of LNCS, , 2017.
	Carlos E. Budde, Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. “JANI: Quantitative Model and Tool Interaction. Proc. of TACAS, Volume of LNCS, , 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, pages 1–53, 2017.
2016
	Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. Proc. of ATVA, Volume 9938 of LNCS, pages 50–67, Springer, 2016.
	Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models. Proc. of Cross-Disciplinary Challenges for Autonomous Systems (CDCAS), Volume of AAAI Technical Reports, AAAI Press, 2016.
	Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis. Proc. of the 35th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP), Volume 9922 of LNCS, pages 253–265, Springer, 2016.
	Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-Reliable Low-Latency Wireless Networks. Proc. of the 35th Symp. on Reliable Distributed Systems (SRDS), pages 307–316, IEEE CS, 2016.
	Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees. Proc. of IEEE/IFIP Symposium on Dependable Systems and Networks (DSN), pages 299-310, IEEE CS, 2016.
	Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs. Proc. of TACAS, Volume 9636 of LNCS, pages 130-146, Springer, 2016.
	Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Abraham, Harold Bruintjes. Parameter Synthesis for Probabilistic Systems. Proc. of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'16), pages 72-74, Albert-Ludwigs-Universität Freiburg, 2016.
Show all

 

External Talks

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.
2016
	Sebastian Junges. Uncovering Dynamic Fault Trees, Talk at DSN'16, 2016.
	Sebastian Junges. Advances and applications of Parameter Synthesis for Probabilistic Systems, Talk at UT Austin, Austin, TX, USA, 2016.
	Sebastian Junges. Advances in parametric probabilistic verification, Talk at QAPL, Eindhoven, The Netherlands, 2016.
Show all