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.
| 2022 | |
|---|---|
[bibtex]
[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. |
| 2021 | |
|
[bibtex]
[issue]
|
, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems, Formal aspects of computing 33 (4/5), pages 637-667, Springer, 2021. |
| Show all | |