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
[bibtex] @conference{PPVISII2023, title = {Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants}, author = {Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja}, booktitle = {LNCS}, volume = {13994}, type = {Conference Paper}, year = {2023}, doi = {10.1007/978-3-031-30820-8_25}, url = { https://publications.rwth-aachen.de/record/957952}, }× [issue]	Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, Tools and Algorithms for the Construction and Analysis of Systems, Volume 13994 of LNCS, 2023.
2022
[bibtex] @article{COPSM2022, title = {Convex Optimization for Parameter Synthesis in MDPs}, author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu}, publisher = {Institute of Electrical and Electronics Engineers}, journal = {IEEE transactions on automatic control}, volume = {67(12)}, pages = {pages 6333-6348}, type = {Journal Article}, year = {2022}, doi = {10.1109/TAC.2021.3133265}, url = { https://publications.rwth-aachen.de/record/888868}, }× [issue]	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.
Show all