Contact

• Office: Room A219, Building 5
• Telephone: +86 10-62661604
• Address: South Fourth Street 4#, Zhong Guan Cun
• Email: <lastname> [at] ios.ac.cn

About me

I am Associate Research Professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. Previously, I was postdoc at Department of Computer Science, University of Oxford and Ph.D. student at Dependable Systems and Software, Universität des Saarlandes. My main research interest is probabilistic model checking. This involves topics such as:

• stochastic hybrid systems
• efficient algorithms for deciding linear time logic properties
• continuous-time Markov chains with infinite state-space
• parametric Markov models
• quantum Markov models

Professional activities

• PC member ICSE 2017 Student Research Competition
• Member of HSCC 2016 Repeatability Evaluation Committee
• Member of HSCC 2014 Repeatability Evaluation Committee
• PC member ValueTools 2013
• Referee for the following journals, conferences, and workshops:
  • Applied Dynamical Systems, SIAM Journal on (SIADS)
  • Applied Mathematics, Journal of (JAM)
  • Automata, Languages and Programming (ICALP)
  • Automated Technology for Verification and Analysis (ATVA)
  • Automated Verification of Critical Systems (AVOCS)
  • Computational Methods in Systems Biology (CMSB)
  • Computer Aided Verification (CAV)
  • Computer Science and Technology, Journal of (JCST)
  • Conference on Concurrency Theory (CONCUR)
  • Dependable Software Engineering: Theories, Tools, and Applications (SETTA)
  • Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy)
  • European Journal of Control (EJCON)
  • Formal Methods (FM)
  • Formal Methods in System Design (FMSD)
  • Formal Modelling and Analysis of Timed Systems (FORMATS)
  • Foundations of Software Technology and Theoretical Computer Science (FSTTCS)
  • Hybrid Systems: Computation and Control (HSCC)
  • Information and Computation, Journal (I&C)
  • Interdisciplinary Sciences: Computational Life Sciences (INSC)
  • Measurement, Modelling and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB & DFT)
  • NASA Formal Methods (NFM)
  • Quantitative Evaluation of SysTems (QEST)
  • Reachability Problems (RP)
  • Science of Computer Programming, Journal (SCICO)
  • Scientific Research and Essays, Journal (SRE)
  • Theoretical Computer Science, Journal (TCS)
  • Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
  • Transactions of Software Engineering, Journal (TSE)
  • Verification, Model Checking, and Abstract Interpretation (VMCAI)

Publications

Google Scholar page: http://scholar.google.de/citations?user=MH7fSVAAAAAJ

• A Simple Algorithm for Solving Qualitative Probabilistic Parity Games, Hahn, E. M.; Schewe, S.; Turrini, A. and Zhang, L. In CAV, pages 291-311, LNCS 9780, 2016.
• A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking, Dijk, T. v.; Hahn, E. M.; Jansen, D. N.; Li, Y.; Neele, T.; Stoelinga, M.; Turrini, A. and Zhang, L. In Dependable Software Engineering: Theories, Tools, and Applications (SETTA), pages 35-51, 2015.
• Lazy Probabilistic Model Checking without Determinisation, Hahn, E. M.; Li, G.; Schewe, S.; Turrini, A. and Zhang, L. In Concurrency Theory (CONCUR), pages 354-367, 2015.
• QPMC: A Model Checker for Quantum Programs and Protocols, Feng, Y.; Hahn, E. M.; Turrini, A. and Zhang, L. In Twentieth international symposium of the Formal Methods Europe association (FM), pages 265-272, Springer, Lecture Notes in Computer Science 9109, 2015.
• Computing Cumulative Rewards Using Fast Adaptive Uniformisation, Dannenberg, F.; Hahn, E. M. and Kwiatkowska, M. Z. In ACM TOMACS, 25: 9, 2015.
• Transient Reward Approximation for Continuous-Time Markov Chains, Hahn, E. M.; Hermanns, H.; Wimmer, R. and Becker, B. In IEEE Transactions on Reliability, 64: 1254-1275, 2015.
• Reachability and Reward Checking for Stochastic Timed Automata, Hahn, E. M.; Hartmanns, A. and Hermanns, H. In AVoCS, 2014.
• Model Checking CSL for Markov Population Models, Spieler, D.; Hahn, E. M. and Zhang, L. In QAPL, pages 93-107, 2014.
• IscasMC: A Web-Based Probabilistic Model Checker, Hahn, E. M.; Li, Y.; Schewe, S.; Turrini, A. and Zhang, L. In Nineteenth international symposium of the Formal Methods Europe association (FM), pages 312-317, Springer, Lecture Notes in Computer Science 8442, 2014.
• Computing Cumulative Rewards Using Fast Adaptive Uniformisation, Dannenberg, F.; Hahn, E. M. and Kwiatkowska, M. Z. In Computational Methods in Systems Biology - 11th International Conference (CMSB), pages 33-49, Springer, Lecture Notes in Computer Science 8130, 2013.
• Model Repair for Markov Decision Processes, Chen, T.; Hahn, E. M.; Han, T.; Kwiatkowska, M.; Qu, H. and Zhang, L. In Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 85-92, IEEE, 2013.
• CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains, Gao, Y.; Hahn, E. M.; Zhan, N. and Zhang, L. In Automated Technology for Verification and Analysis - 11th International Symposium (ATVA), pages 464-468, Springer, Lecture Notes in Computer Science 8172, 2013.
• Rewarding probabilistic hybrid automata, Hahn, E. M. and Hermanns, H. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 313-322, ACM, 2013.
• A compositional modelling and analysis framework for stochastic hybrid systems, Hahn, E. M.; Hartmanns, A.; Hermanns, H. and Katoen, J.-P. In Formal Methods in System Design, 43: 191-232, 2013.
• Model Checking for Performability, Baier, C.; Hahn, E. M.; Haverkort, B. R. and Katoen, H. H. J.-P. In Mathematical Structures in Computer Science, 23: 751-795, 2013.
• Variable Probabilistic Abstraction Refinement, Fioriti, L. M. F.; Hahn, E. M.; Hermanns, H. and Wachter, B. In Automated Technology for Verification and Analysis - 10th International Symposium (ATVA), pages 300-316, Springer, Lecture Notes in Computer Science 7561, 2012.
• Safety Verification for Probabilistic Hybrid Systems, Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H. and Hahn, E. M. In European Journal of Control, 18: 572-587, 2012.
• Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems, Hahn, E. M.; Norman, G.; Parker, D.; Wachter, B. and Zhang, L. In Eighth International Conference on Quantitative Evaluation of Systems (QEST), pages 69-78, IEEE Computer Society, 2011.
• Reachability analysis for incomplete networks of Markov decision processes, Wimmer, R.; Hahn, E. M.; Hermanns, H. and Becker, B. In 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pages 151-160, IEEE, 2011.
• Model Checking Algorithms for CTMDPs, Buchholz, P.; Hahn, E. M.; Hermanns, H. and Zhang, L. In Computer Aided Verification - 23rd International Conference (CAV), pages 225-242, Springer, Lecture Notes in Computer Science 6806, 2011.
• Bounded Fairness for Probabilistic Distributed Algorithms, Crouzen, P.; Hahn, E. M.; Hermanns, H.; Dhama, A.; Theel, O. E.; Wimmer, R.; Braitling, B. and Becker, B. In 11th International Conference on Application of Concurrency to System Design (ACSD), pages 89-97, IEEE, 2011.
• Synthesis for PCTL in Parametric Markov Decision Processes, Hahn, E. M.; Han, T. and Zhang, L. In NASA Formal Methods - Third International Symposium (NFM), pages 146-161, Springer, Lecture Notes in Computer Science 6617, 2011.
• Measurability and safety verification for stochastic hybrid systems, Fränzle, M.; Hahn, E. M.; Hermanns, H.; Wolovick, N. and Zhang, L. In Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 43-52, ACM, 2011.
• The ins and outs of the probabilistic model checker MRMC, Katoen, J.-P.; Zapreev, I. S.; Hahn, E. M.; Hermanns, H. and Jansen, D. N. In Performance Evaluation, 68: 90-104, 2011.
• Probabilistic Reachability for Parametric Markov Models, Hahn, E. M.; Hermanns, H. and Zhang, L. In STTT, 13: 3-19, 2011.
• Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains, Calin, G.; Crouzen, P.; D'Argenio, P. R.; Hahn, E. M. and Zhang, L. In Model Checking Software - 17th International SPIN Workshop, pages 193-211, Springer, Lecture Notes in Computer Science 6349, 2010.
• Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems, Wimmer, R.; Braitling, B.; Becker, B.; Hahn, E. M.; Crouzen, P.; Hermanns, H.; Dhama, A. and Theel, O. E. In Seventh International Conference on the Quantitative Evaluation of Systems (QEST), pages 27-36, IEEE Computer Society, 2010.
• Safety Verification for Probabilistic Hybrid Systems, Zhang, L.; She, Z.; Ratschan, S.; Hermanns, H. and Hahn, E. M. In Computer Aided Verification, 22nd International Conference (CAV), pages 196-211, Springer, Lecture Notes in Computer Science 6174, 2010.
• PARAM: A Model Checker for Parametric Markov Models, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Computer Aided Verification, 22nd International Conference (CAV), pages 660-664, Springer, Lecture Notes in Computer Science 6174, 2010.
• PASS: Abstraction Refinement for Infinite Probabilistic Models, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference (TACAS), pages 353-357, Springer, Lecture Notes in Computer Science 6015, 2010.
• The Ins and Outs of the Probabilistic Model Checker MRMC, Katoen, J.-P.; Zapreev, I. S.; Hahn, E. M.; Hermanns, H. and Jansen, D. N. In Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 167-176, IEEE Computer Society, 2009.
• Probabilistic Reachability for Parametric Markov Models, Hahn, E. M.; Hermanns, H. and Zhang, L. In Model Checking Software, 16th International SPIN Workshop, pages 88-106, Springer, Lecture Notes in Computer Science 5578, 2009.
• INFAMY: An Infinite-State Markov Model Checker, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Computer Aided Verification, 21st International Conference (CAV), pages 641-647, Springer, Lecture Notes in Computer Science 5643, 2009.
• Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains, Hahn, E. M.; Hermanns, H.; Wachter, B. and Zhang, L. In Fundamenta Informaticae, 95: 129-155, 2009.
• Time-bounded model checking of infinite-state continuous-time Markov chains, Zhang, L.; Hermanns, H.; Hahn, E. M. and Wachter, B. In 8th International Conference on Application of Concurrency to System Design (ACSD), pages 98-107, IEEE, 2008.
• Towards a Unified Model-Based Safety Assessment, Peikenkamp, T.; Cavallo, A.; Valacca, L.; Böde, E.; Pretzer, M. and Hahn, E. M. In Computer Safety, Reliability, and Security, 25th International Conference (SAFECOMP), pages 275-288, Springer, Lecture Notes in Computer Science 4166, 2006.

Thesis

• Model checking stochastic hybrid systems, Hahn, E. M. Ph.D. Thesis, Universität des Saarlandes, 2013.

Student projects

Christian Josef Köhl: Probabilistische Aspekte – AspectKP – ein verteiltes Prozesskalkül

Teaching activities

• SS11: Tutor for the lecture Data Networks by Prof. Dr.-Ing. Holger Hermanns
• WS10/11: Assistant for the proseminar Im Zoo der Automaten by Prof. Dr.-Ing. Holger Hermanns
• SS10: Assistant for the advanced course Quantitative Model Checking by Prof. Dr.-Ing. Holger Hermanns
• SS09: Assistant for the advanced course Quantitative Model Checking by Dr. Lijun Zhang
• WS08/09: Assistant for the advanced course Testing Techniques by Prof. Dr.-Ing. Holger Hermanns and Dr. Julien Schmaltz
• WS08/09: Assistant for the proseminar Im Zoo der Automaten by Prof. Dr.-Ing. Holger Hermanns
• SS08: Student assistant for the lecture Nebenläufige Programmierung by Prof. Dr.-Ing. Holger Hermanns
• SS07: Student assistant for the lecture Embedded Systems by Prof. Bernd Finkbeiner, Ph.D.

Participation in tool development

I have contributed to the development of the following tools:

• IscasMC (main developer)
• CCMC (participation in tool paper and internal review of homepage)
• PARAM (main developer)
• ProHVer (main developer)
• INFAMY (main developer)
• PASS (improvements on value iteration and code cleanup)
• PRISM (integration of parametric analysis and an extension of the fast adaptive uniformisation, see the development version 4.1.dev.r7596)
• MRMC (integration of two algorithms on continuous-time Markov decision processes)

My work also involves several smaller tools developed for single publications.

Participation in Projects in the past

• CAP – “Composition, Abstraction, and Parametrization for the Verification of Probabilistic Hybrid Systems”, Chinesisch-Deutsches Zentrum für Wissenschaftsförderung (CDZ)
• VERIWARE (University of Oxford)
• AVACS (S2, S3, H4) (Universität des Saarlandes)
• Quasimodo (Universität des Saarlandes)
• ROCKS (Universität des Saarlandes)
• ISAAC (OFFIS)

Education

• May 2013: Doctoral degree (Dr.-Ing.) “summa cum laude” from Universität des Saarlandes (defence: 21.12.2012)
• April 2008: Second degree in Computer Science (Master) “with honours” received from Universität des Saarlandes
• September 2005: First degree in Computer Science (Bachelor) received from Carl von Ossietzky Universität Oldenburg
• 5/2008 – 10/2012: Studying Computer Science (Ph.D.) at Universität des Saarlandes
• 10/2006 – 4/2008: Studied Computer Science (Master) at Universität des Saarlandes
• 10/2002 – 9/2005: Studied Computer Science (Bachelor) with minors in Mathematics at Carl von Ossietzky Universität Oldenburg
• 8/1995 – 6/2002: Abitur at Altes Gymnasium Oldenburg

Professional Appointments

• since 6/2013: Associate Research Professor at State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
• 10/2012 – 5/2013: Research Assistant at University of Oxford
• 5/2010 – 10/2012: Research Assistant at Universität des Saarlandes
• 10/2005 – 10/2006: Research Assistant at OFFIS, Safety Analysis & Verification (Oldenburg)

Scholarships and Affiliations

• since 12/2013: Project “Model Checking of Complex and Hybrid Stochastic Systems”, Grant No. 61350110518, 61450110461, 61550110506 of Research Fund for International Young Scientists (extended two times)
• since 6/2013: Chinese Academy of Sciences fellowship for young international scientists, Grant No. 2013Y1GB0006 (extended two times)
• 1/2013 – 5/2013: Member of Common Room of Wolfson College, Oxford
• 2/2010 – 4/2010: Exchange in Argentina within the programme “Projektbezogener Personenaustausch mit Argentinien (PROALAR)” by the Deutscher Akademischer Austauschdienst (DAAD) and the Ministerio de Ciencia, Tecnología e Innovacíon Productiva (MINCyT)
• 5/2008 – 4/2010: Scholarship of the graduate school “Leistungsgarantien für Rechnersysteme” of the Deutsche Forschungsgemeinschaft
• 2009: Faculty Nomination for a stipend of the “Deutsche Telekom Stiftung“

Personal Data

• Full Name: Ernst Moritz Hahn
• Date of Birth: October 3rd, 1982
• Place of Birth: Fernwald, Germany (Hesse)

Language proficiency

• German: native speaker
• English: highly proficient in spoken and written language
• Chinese (Mandarin): good command