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

Publications for Sebastian Junges

2019
	Milan Ceska, Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches. Proc. of FM, , 2019.
	Tobias Winkler, Sebastian Junges, Guillermo A Perez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes. Proc. of CONCUR, , 2019.
	Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees. Reliability Engineering and System Safety 186, pages 37–50, 2019.
	Milan Ceska, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains. Proc. of TACAS, Volume of LNCS, , 2019.
2018
	Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters. Proc. of ATVA, Volume 11138 of LNCS, pages 160-176, Springer, 2018.
	Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking For Safe Navigation Among Humans. Proc. of QEST, Volume of LNCS, , 2018.
	Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs via Parameter Synthesis. Proc. of UAI, AUAI, 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 10877 of LNCS, pages 272–293, 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.
Show all

 

External Talks

Show all