I'm Dennis Guck,
a PhD student (AIO)

in the Formal Methods and Tools group
of the Department of Computer Science
at the University of Twente.

Research

Also see my DBLP page, my Google Scholar Citations page and my EEMCS EPrints page.

Publications

2016

Giannakopoulou, D. and Guck, D. and Schumann, J. (2016) Exploring Model Quality for ACAS X. In: Proceedings of the 21 International Symposium on Formal Methods, FM 2016, 07-11 Nov 2016, Limassol, Cyprus.
Ruijters, E.J.J. and Guck, D. and Drolenga, P. and Peters, M. and Stoelinga, M.I.A. (2016) Maintenance analysis and optimization via statistical model checking: Evaluating a train pneumatic compressor. In: Proceedings of the 13th International Conference on Quantitative Evaluation of SysTems, QEST 2016, 23-25 Aug 2016, Québec City, Canada.
Ruijters, E.J.J. and Guck, D. and Drolenga, P. and Stoelinga, M.I.A. (2016) Fault maintenance trees: reliability centered maintenance via statistical model checking. In: Proceedings of the IEEE 62nd Annual Reliability and Maintainability Symposium, RAMS 2016, 25-28 Jan 2016, Tucson, AZ, USA. IEEE.
Junges, S., Guck, D., Katoen, J.P. and Stoelinga, M., 2016. Uncovering Dynamic Fault Trees. In: Proceedings of the 46th annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016, 28 Jun - 01 Jul 2016, Toulouse, France.
Ruijters, E.J.J. and Guck, D. and van Noort, M. and Stoelinga, M.I.A. (2016) Reliability-centered maintenance of the Electrically Insulated Railway Joint via Fault Tree Analysis: A practical experience report. In: Proceedings of the 46th annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2016, 28 Jun - 01 Jul 2016, Toulouse, France.

2015

Arnold, F. and Guck, D. and Kumar, R. and Stoelinga, M.I.A. (2015) Sequential and Parallel Attack Tree Modelling. In: Computer Safety, Reliability, and Security - Proceedings of the SAFECOMP 2015 Workshops, ASSURE, DECSoS. ISSE, ReSA4CI, and SASSUR, 22 September 2015, Delft, The Netherlands. pp. 291-299. Lecture Notes in Computer Science 9338. Springer Verlag.
Guck, D. and Spel, J.J. and Stoelinga, M.I.A. (2015) DFTCalc: Reliability centered maintenance via fault tree analysis (tool paper). In: Proceedings of the 17th International Conference on Formal Engineering Methods (ICFEM 2015), 03-06 Nov 2015, Paris, France. pp. 304-311. Lecture Notes in Computer Science 9407. Springer Verlag.
Junges, S. and Guck, D. and Katoen, J.P. and Rensink, A. and Stoelinga, M.I.A. (2015) Fault Trees on a Diet - Automated Reduction by Graph Rewriting. In: Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015), 4-6 Nov 2015, Nanjing, China. pp. 3-18. Lecture Notes in Computer Science 9409. Springer Verlag.

2014

A. Arnold, D. Gebler, D. Guck, H. Hatefi: A Tutorial on Interactive Markov Chains. In Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, pp. 26-66. Springer Berlin Heidelberg, 2014.
Guck, D. and Timmer, M. and Hatefi, H and Ruijters, E.J.J. and Stoelinga, M.I.A. (2014) Modelling and analysis of Markov reward automata. In: Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis (ATVA 2014), 03-07 November 2014, Sydney, Australia, pp. 168-184. Lecture Notes in Computer Science 8837. Springer Verlag.
D. Guck, H. Hatefi, H. Hermanns, J.-P. Katoen, M. Timmer: Analysis of Timed and Long-Run Objectives for Markov Automata. Logical Methods in Computer Science 10(3) (2014)
D. Guck, J.-P. Katoen, M.I.A. Stoëlinga, T. Luiten, J. Romijn. Smart Railroad Maintenance Engineering with Stochastic Model Checking. In Proceedings of the Second International Conference on Railway Technology: Research, Development and Maintenance. Civil-Comp Press, Stirlingshire, UK, Paper 299, 2014.

2013

Arnold, F. and Belinfante, A.F.E. and Van der Berg, F.I. and Guck, D. and Stoelinga, M.I.A. DFTCalc: A Tool for Efficient Fault Tree Analysis. In 32nd Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP’13). LNCS. Springer, 2013.
Guck D. and Hatefi H. and Hermanns H. and Katoen J.-P. and Timmer M. Modelling, Reduction and Analysis of Markov Automata. In 10th Int. Conf. on Quantitative Evaluation of Systems (QEST’13). LNCS. Springer, 2013.

2012

Guck, D. and Han, T. and Katoen, J.P. and Neuhäußer, M.R. (2012) Quantitative Timed Analysis of Interactive Markov Chains. In NASA Formal Methods Symposium (NFM). pages 8–23. Volume 7226 of Lecture Notes in Computer Science. Springer-Verlag.

Technical reports

2014

Guck, D. and Timmer, M. and Hatefi, H and Ruijters, E.J.J. and Stoelinga, M.I.A. (2014) Modelling and analysis of Markov reward automata (extended version).Technical Report TR-CTIT-14-06, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625

2013

Arnold, F. and Belinfante, A.F.E. and Van der Berg, F.I. and Guck, D. and Stoelinga, M.I.A. (2013) DFTCalc: a tool for efficient fault tree analysis (extended version).Technical Report TR-CTIT-13-13, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625
Guck, D. and Hatefi, H. and Hermanns, H. and Katoen, J.-P. and Timmer, M. (2013) Modelling, Reduction and Analysis of Markov Automata (extended version), CoRR abs/1305.7050

Workshops

2015

Kumar, R. and Guck, D. and Stoelinga, M.I.A. (2015) Time dependent analysis with dynamic counter measure trees. In: Proceedings of the 13th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2015), 11-12 April 2015, London, England. pp. 1-5. Inria.

2014

Guck, D. and Timmer, M. and Blom, S.C.C. (2014) Extending Markov Automata with State and Action Rewards. In: Proceedings of the 12th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), 12-13 April 2014, Grenoble, France. Inria.

Theses

2012

Guck, D. (2012) Quantitative Analysis of Markov Automata. Master's thesis, RWTH Aachen University.

2010

Guck, D. (2010) Analysis and scheduler synthesis of time-bounded reachability in continuous-time Markov decision processes. Bachelor's thesis, RWTH Aachen University.

Selected Talks

2013

Fault Tree Analysis for Railroad Maintenance. IPA Spring Days on Cyber-Physical Systems 2013, Groesbeck, Netherlands, 14 May 2013.
Modelling, Reduction and Analysis of Dynamic Fault Trees. ROCKS meeting 2013, Fulda, Germany, 11 April 2013.
Modelling, Reduction and Analysis of Markov Automata. Sensation meeting 2013, Saarbrücken, Germany, 10 April 2013.

2012

Quantitative Timed Analysis of Interactive Markov Chains. In NASA Formal Methods Symposium (NFM) 2012, Norfolk, Virginia, USA, 4 April 2012.

Events attended

Conferences / Workshops

  • The 12th International Symposium on Automated Technology for Verification and Analysis (ATVA) 2014, Sydney, Australia, 03-07 November 2014
  • The 12th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL) 2014, Grenoble, France, April 12-13, 2014 at ETAPS 2014
  • The 2nd International Conference on Railway Technology: Research, Development and Maintenance, Ajaccio, Corsica, France, 8-11 April 2014
  • The 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP) 2013, Toulouse, France, September 2013.
  • 10th International Conference on Quantitative Evaluation of SysTems (QEST) 2013, Buenos Aires, Argentina, August 2013.
  • The European Joint Conferences on Theory and Practice of Software (ETAPS) 2013, Rome, Italy, March 2013.
  • NASA Formal Methods Symposium (NFM) 2012, Norfolk, Virginia, USA, April 2012.
  • The European Joint Conferences on Theory and Practice of Software (ETAPS) 2011, Saarbrücken, Germany, March/April 2011.

Selected seminars / summer schools

  • Marktoberdorf Summer School, Dependable Software Systems Engineering, Marktoberdorf, Germany, August 2014
  • Dagstuhl seminar 14031, Randomized Timed and Hybrid Models for Critical Infrastructures, Schloss Dagstuhl, Germnay, January 2014
  • ROCKS Autumn School, Vahrn, Italy, October 2012.

Selected meetings

  • ROCKS meeting, Slenaken, Netherlands, November 2013.
  • Sensation meeting, Enschede, Netherlands, October 2013.
  • IPA Spring Days on Cyber-Physical Systems 2013, Groesbeck, Netherlands, May 2013.
  • ROCKS meeting, Fulda, Germany, April 2013.
  • Sensation meeting, Saarbrücken, Germany, April 2013.

PhD project

ArRangeer: smARt RAilroad maintenance eNGinEEring
with stochastic model checking


Keywords

FMT

Project Poster

ExploRail

DFTCalc

Tools

IMCA (Interactive Markov Chain Analyzer) is a tool for the quantitative analysis of Markov automata (MA).
In particular, it supports the verification of MAs against:

  • Timed reachability objectives.
  • Reachability objectives.
  • Expected time and reward objectives.
  • Long-run average objectives.

The newest developments of the tool can be found in the IMCA github repository.
The newest stable release can be found in FMTs IMCA gitub repository.
To find out more about IMCA, visit the official homepage (no current release).

Projects using IMCA:

Contact

  • Address

    University of Twente
    EWI-FMT (Zilverling)
    P.O. Box 217
    7500 AE Enschede
    The Netherlands