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.
Show all

 

External Talks

Show all