You are here: Home Team Daniel Dietsch

Daniel Dietsch


Research Interests

Requirements, Static Analysis, Modeling, Processes, Formal Methods in Practice


Please visit my Google Scholar profile or DBLP.




Consultation Hours

Please contact me for an appointment. 

Student Projects and Thesis Topics

Please see our available topics in the context of Ultimate and our shared overview for thesis topics and student projects for an up-to-date list of available topics and projects. If you have questions about topics I offer there, feel free to write me an email or come over to my office.

Also, if you have your own topic and search for an advisor, feel free to ask me. 


  • Software Lab (Summer Term 2009, 2010, 2011, 2012, 2013, 2014, 2015)
  • Software Lab for members of all faculties (Winter Term 2009/2010, 2010/2011, 2011/2012, 2012/2013, 2013/2014)
  • Seminar: Formal Methods for C (Summer Term 2014)
  • Seminar Advanced Topics in Requirements Engineering (Summer Term 2013)
  • Seminar Static Code Analysis (Winter Term 2009/2010, 2010/2011, 2011/2012)
  • Seminar Requirements Engineering (Summer Term 2012)


  • Software Lab (Summer Term 2007, 2008)
  • Software Lab for members of all faculties (Winter Term 2007/2008, 2008/2009)
  • Integratives BOK Projekt "Sichere Systeme" (Winter Term 2007/2008, 2008/2009)
  • Software Design, Modelling and Analysis in UML (Winter Term 2008/2009)
  • Real-Time Systems (Summer Term 2009)
  • Informatik I (Winter Term 2007/2008, 2008/2009)
  • Programmierzertifikat Objekt-Orientierung mit Java (Summer Term 2008

Supervised Student Projects and Theses


  • Schätzle, C.: Octagon Domain for Ultimate. Bachelor Thesis (In Progress).
  • Hättig, J.: Convex Polyhedra as Abstract Domain for Abstract Interpretation in Ultimate. Master Thesis.
  • Meyer, B.: Automatisierung des Authoring-Prozesses für gesundheitsbezogene Ratgeber-Apps. Bachelor Thesis.
  • Fordinal, G.: A New Webinterface for Ultimate. Bachelor Project.


  • Szymanski, U.: Model-based Verification of State-Machine Implementations with Microsoft VCC. Master Thesis.
  • Dillo, C.: Modular Abstract Interpretation for Ultimate. Bachelor Thesis.
  • Schillinger, F.: Adapting Abstract Interpretation for Nested Word Automata. Master Project.
  • Schätzle, C.: Boogie Procedure Inlining. Bachelor Project.


  • Langenfeld, V.: LTL Software Model Checking with Büchi Programs. Master Thesis.
  • Dzienian, J.: Continuous Integration and Testing for Ultimate. Master Project.
  • Cheng, T.-N., Hättig, J., Holub, J., and Schillinger, F.: Advanced Video Game Architecture. Master Team Project.


  • Dzienian, J. and Langenfeld, V.: Cookify - Temporal Property Verification for Boogie. Master Team Project.
  • Hofmann, C.: Verification as a Service. Bachelor Thesis.
  • Metzger, J.: Anforderungsanalyse für eine mobile medizinische Ratgeberapplikation. Bachelor Thesis.
  • Lindemann, M., Saukh, O., and Wissert, S.: C+ACSL to Boogie compiler, Eclipse CDT integration and web-interface development as part of the Ultimate project. Master Team Project.
  • Maier, C.: Formal Verification of Embedded Systems using VCC. Master Team Project.


  • Hummel, S..: The Delphi Method - An Appropriate Approach to Requirements Elicitation? Bachelor Thesis.
  • Kacmaz, G.: Ermittlung und Pflege eines Softwareproduktkerns anhand des CaVE-Ansatzes. Bachelor Thesis.
  • Dzienian, J.: Empirische Studie zur Verbesserung der Bedienfreundlichkeit von Spielen für mobile Endgeräte. Bachelor Thesis.
  • Blank A. and Greitschus M.: Infrastructure for Inferring Verification Annotations in C Programs. Master Team Project.
  • Mahdi A. and Jubran O.: Formal Analysis of Message Collision due to Clock Drift and Dynamic Message Scheduling in a Wireless Sensor Network. Master Team Project.
  • Butt, D.: Towards Risk Mitigation in Critical Software Development: Introducing MBD in SMEs. Master Thesis.