Christian Hensel | Informatik 2

Email: dehnert at cs.rwth-aachen.de
Address: Room 4210
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21203

I am a PhD student at the Software Modeling and Verification Group (MOVES) headed by Professor J.-P. Katoen.
My research interests include:

formal methods for qualitative and quantitative systems
abstraction techniques for quantitative systems
symbolic methods for the analysis of systems
SMT-solving, in particular its applications to the analysis of formal models

2024
[bibtex] @article{PM2024, title = {Parameter synthesis for Markov models: covering the parameter space}, author = {Sebastian Junges and Erika Ábrahám and Hans Christian Hensel and Nils Jansen and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk}, publisher = {Springer}, journal = {Formal methods in system design}, volume = {62(1/3)}, pages = {pages 181-259}, type = {Journal Article}, year = {2024}, doi = {10.1007/s10703-023-00442-x}, url = { https://publications.rwth-aachen.de/record/985754}, }× [issue]	Sebastian Junges, Erika Ábrahám, Hans Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. Parameter synthesis for Markov models: covering the parameter space, Formal methods in system design 62 (1/3), pages 181-259, Springer, 2024.
2021
[bibtex] @article{C2021, title = {Counterexample-guided inductive synthesis for probabilistic systems}, author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen}, publisher = {Springer}, journal = {Formal aspects of computing}, volume = {33(4/5)}, pages = {pages 637-667}, type = {Journal Article}, year = {2021}, doi = {10.1007/s00165-021-00547-2}, url = { https://publications.rwth-aachen.de/record/820111}, }× [issue]	Milan Češka, 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.
[bibtex] @article{TS2021, title = {The probabilistic model checker STORM}, author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk}, publisher = {Springer}, journal = {International journal on software tools for technology transfer}, volume = {24(4)}, pages = {pages 589-610}, type = {Journal Article}, year = {2021}, doi = {10.1007/s10009-021-00633-z}, url = { https://publications.rwth-aachen.de/record/822059}, }× [issue]	Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer 24 (4), pages 589-610, Springer, 2021.
2020
[bibtex] @article{PMPG2020, title = {Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination}, author = {Christel Baier and Hans Christian Hensel and Lisa Hutschenreiter and Sebastian Junges and Joost-Pieter Katoen and Joachim Klein}, publisher = {Elsevier}, journal = {Information and computation}, volume = {272}, pages = {pages 104504}, type = {Journal Article}, year = {2020}, doi = {10.1016/j.ic.2019.104504}, url = { https://publications.rwth-aachen.de/record/793292}, }× [issue]	Christel Baier, Hans Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein. Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Information and computation 272, pages 104504, Elsevier, 2020.
2019
[bibtex] @conference{TCTAQFMQCR2019, title = {The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models: (QComp 2019 Competition Report)}, author = {Ernst Moritz Hahn and Arnd Hartmanns and Hans Christian Hensel and Michaela Klauck and Joachim Klein and Jan Křetínský and David Parker and Tim Quatmann and Enno Ruijters and Marcel Steinmetz}, publisher = {Springer}, booktitle = {LNCS}, volume = {11429}, pages = {69-92}, type = {Conference Paper}, year = {2019}, doi = {10.1007/978-3-030-17502-3_5}, url = { https://publications.rwth-aachen.de/record/759255}, }× [issue]	Ernst Moritz Hahn, Arnd Hartmanns, Hans Christian Hensel, Michaela Klauck, Joachim Klein, Jan Křetínský, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models: (QComp 2019 Competition Report), 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11429 of LNCS, 69-92, Springer, 2019.
[bibtex] @inbook{MRR2019, title = {Model Repair Revamped}, author = {Milan Češka and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {11500}, pages = {107-125}, type = {Book Chapter}, year = {2019}, doi = {10.1007/978-3-030-31514-6_7}, url = { https://publications.rwth-aachen.de/record/768054}, }× [issue]	Milan Češka, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019.
[bibtex] @conference{CDSPPS2019, title = {Counterexample-Driven Synthesis for Probabilistic Program Sketches}, author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {11800}, pages = {101-120}, type = {Conference Paper}, year = {2019}, doi = {10.1007/978-3-030-30942-8_8}, url = { https://publications.rwth-aachen.de/record/786831}, }× [issue]	Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3. World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019.
2018
[bibtex] @phdthesis{TS2018, title = {The probabilistic model checker Storm: symbolic methods for probabilistic model checking}, author = {Hans Christian Hensel}, publisher = {RWTH Aachen University, Department of Computer Science}, booktitle = {Aachener Informatik-Berichte}, volume = {2018-06}, institution = {RWTH Aachen University}, pages = {1 Online-Ressource (vii, 331 Seiten) : Illustrationen}, type = {PhD Thesis}, year = {2018}, doi = {10.18154/RWTH-2018-231803}, url = { https://publications.rwth-aachen.de/record/752011}, }× [issue]	Hans Christian Hensel. The probabilistic model checker Storm: symbolic methods for probabilistic model checking, PhD Thesis, RWTH Aachen University, Volume 2018-06 of Aachener Informatik-Berichte, 1 Online-Ressource (vii, 331 Seiten) : Illustrationen, RWTH Aachen University, Department of Computer Science, 2018.
2017
[bibtex] @unpublished{ACAMPMC2017, title = {A storm is Coming: A Modern Probabilistic Model Checker}, author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk}, pages = {14 Seiten : Tabellen, Diagramme}, type = {Preprint}, year = {2017}, url = { https://arxiv.org/abs/1702.04311}, }× [issue]	Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311
[bibtex] @conference{ASCAMPMC2017, title = {A Storm is Coming: A Modern Probabilistic Model Checker}, author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk}, publisher = {Springer}, booktitle = {LNCS}, volume = {10427}, pages = {592-600}, type = {Conference Paper}, year = {2017}, doi = {10.1007/978-3-319-63390-9_31}, url = { https://publications.rwth-aachen.de/record/713569}, }× [issue]	Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, 29. International Conference on Computer-Aided Veriﬁcation (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
[bibtex] @conference{JQMTI2017, title = {JANI: Quantitative Model and Tool Interaction}, author = {Carlos E. Budde and Hans Christian Dehnert and E. Moritz Hahn and Arnd Hartmanns and Sebastian Junges and Andrea Turrini}, publisher = {Springer}, booktitle = {LNCS}, volume = {10206}, pages = {151-168}, type = {Conference Paper}, year = {2017}, doi = {10.1007/978-3-662-54580-5_9}, url = { https://publications.rwth-aachen.de/record/713573}, }× [issue]	Carlos E. Budde, Hans Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. JANI: Quantitative Model and Tool Interaction, 23. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 151-168, Springer, 2017.
2016
[bibtex] @conference{PSMMFTE2016, title = {Parameter Synthesis for Markov Models: Faster Than Ever}, author = {Tim Quatmann and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9938}, pages = {50-67}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-46520-3_4}, url = { https://publications.rwth-aachen.de/record/681503}, }× [issue]	Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
[bibtex] @conference{BMCPP2016, title = {Bounded Model Checking for Probabilistic Programs}, author = {Nils Jansen and Hans Christian Dehnert and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Lukas Westhofen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9938}, pages = {68-85}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-319-46520-3_5}, url = { https://publications.rwth-aachen.de/record/681511}, }× [issue]	Nils Jansen, Hans Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, 68-85, Springer, 2016.
[bibtex] @conference{P2016, title = {Parameter synthesis for probabilistic systems}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Albert-Ludwigs-Universität}, pages = {72-74}, type = {Conference Paper}, year = {2016}, doi = {10.6094/UNIFR/10639}, url = { https://publications.rwth-aachen.de/record/683021}, }× [issue]	Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
[bibtex] @conference{SRLM2016, title = {Safety-constrained Reinforcement Learning for MDPs}, author = {Sebastian Junges and Nils Jansen and Hans Christian Dehnert and Ufuk Topcu and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {9636}, pages = {130-146}, type = {Conference Paper}, year = {2016}, doi = {10.1007/978-3-662-49674-9_8}, url = { https://publications.rwth-aachen.de/record/684642}, }× [issue]	Sebastian Junges, Nils Jansen, Hans Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs, 22. international conference, held as part of the European Joint Conferences on Theory and Practice of Software (TACAS 2016), Volume 9636 of LNCS, 130-146, Springer, 2016.
2015
[bibtex] @conference{CER2015, title = {Counterexamples for Expected Rewards}, author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker}, publisher = {Springer}, booktitle = {LNCS}, volume = {9109}, pages = {435-452}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-19249-9_27}, url = { https://publications.rwth-aachen.de/record/541095}, }× [issue]	Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, 20. international symposium Formal Methods (FM 2015), Volume 9109 of LNCS, 435-452, Springer, 2015.
[bibtex] @conference{PAPPST2015, title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool}, author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám}, publisher = {Springer}, booktitle = {LNCS}, volume = {9206}, pages = {214-231}, type = {Conference Paper}, year = {2015}, doi = {10.1007/978-3-319-21690-4_13}, url = { https://publications.rwth-aachen.de/record/564236}, }× [issue]	Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
2014
[bibtex] @conference{CGDTMMAIS2014, title = {Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey}, author = {Erika Ábrahám and Bernd Becker and Hans Christian Dehnert and Nils Jansen and Joost-Pieter Katoen and Ralf Wimmer}, publisher = {Springer}, booktitle = {LNCS}, volume = {8483}, pages = {65-121}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-07317-0_3}, url = { https://publications.rwth-aachen.de/record/443312}, }× [issue]	Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey, Formal methods for executable software models (SFM 2014), Volume 8483 of LNCS, 65-121, Springer, 2014.
[bibtex] @conference{FDPM2014, title = {Fast Debugging of PRISM Models}, author = {Hans Christian Dehnert and Nils Jansen and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {8837}, pages = {146-162}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-319-11936-6_11}, url = { https://publications.rwth-aachen.de/record/460136}, }× [issue]	Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. Fast Debugging of PRISM Models, Automated technology for verification and analysis : 12th international symposium (ATVA 2014), Volume 8837 of LNCS, 146-162, Springer, 2014.
[bibtex] @conference{OAPS2014, title = {On Abstraction of Probabilistic Systems}, author = {Hans Christian Dehnert and Daniel Gebler and Michele Volpato and David N. Jansen}, publisher = {Springer}, booktitle = {LNCS}, volume = {8453}, pages = {87-116}, type = {Conference Paper}, year = {2014}, doi = {10.1007/978-3-662-45489-3_4}, url = { https://publications.rwth-aachen.de/record/465752}, }× [issue]	Hans Christian Dehnert, Daniel Gebler, Michele Volpato, David N. Jansen. On Abstraction of Probabilistic Systems, Stochastic model checking (ROCKS 2012), Volume 8453 of LNCS, 87-116, Springer, 2014.
2013
[bibtex] @conference{SBMMM2013, title = {SMT-based Bisimulation Minimisation of Markov Models}, author = {Hans Christian Dehnert and David Parker and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {7737}, pages = {28-47}, type = {Conference Paper}, year = {2013}, doi = {10.1007/978-3-642-35873-9_5}, url = { https://publications.rwth-aachen.de/record/225435}, }× [issue]	Hans Christian Dehnert, David Parker, Joost-Pieter Katoen. SMT-based Bisimulation Minimisation of Markov Models, Verification, Model Checking, and Abstract Interpretation [Elektronische Ressource] : 14. International Conference (VMCAI), Volume 7737 of LNCS, 28-47, Springer, 2013.