Christian Hensel

like-a-sir150px
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
2019
DOI fulltext PDF [bibtex]
@conference{TCTAQFM2019,
title = {The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models},
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, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11429 of LNCS, 69-92, Springer, 2019.
DOI [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, 3rd World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019.
2018
DOI fulltext PDF [bibtex]
@phdthesis{TS2018,
title = {The probabilistic model checker Storm},
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, 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
DOI [bibtex]
@conference{J2017,
title = {JANI},
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, 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 151-168, Springer, 2017.
DOI [bibtex]
@conference{ASC2017,
title = {A Storm is Coming},
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, 29th International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
2016
DOI [bibtex]
@conference{PSMM2016,
title = {Parameter Synthesis for Markov Models},
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, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
DOI [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, 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, 68-85, Springer, 2016.
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 9636 of LNCS, 130-146, Springer, 2016.
2015
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 9109 of LNCS, 435-452, Springer, 2015.
DOI [bibtex]
@conference{P2015,
title = {PROPhESY},
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, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
2014
DOI [bibtex]
@inbook{CGDTMM2014,
title = {Counterexample Generation for Discrete-Time Markov Models},
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 = {Book Chapter},
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, Volume 8483 of LNCS, 65-121, Springer, 2014.
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 8837 of LNCS, 146-162, Springer, 2014.
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 8453 of LNCS, 87-116, Springer, 2014.
2013
DOI [bibtex]
@inbook{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 = {Book Chapter},
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, Volume 7737 of LNCS, 28-47, Springer, 2013.