We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
2 papers accepted at ASE 2024: BenchCloud and CoVeriTeam GUI
activities-university-web

Teaching

Instruction at Ludwig-Maximilians-Universität München

Undergraduate courses

  1. Software Engineering
    Winter 2016/17, Winter 2017/18, Winter 2018/19, Winter 2020/21, Winter 2021/22
  2. Formal Specification and Verification
    Summer 2017, Summer 2018
  3. Formale Sprachen und Komplexität
    Summer 2020
  4. Theoretische Informatik für Medieninformatiker
    Summer 2020

Graduate courses

  1. Semantics for Programming Languages
    Winter 2019/20, Winter 2020/21, Winter 2021/22
  2. Testing
    Summer 2018, Summer 2019, Summer 2020, Summer 2021, Summer 2022
  3. Software Analysis and Verification
    Winter 2020/21, Winter 2021/22
  4. Software Verification
    Winter 2018/19, Winter 2019/20
  5. Formal Specification and Verification II
    Winter 2017/18
  6. Science and Practice in Software Engineering
    Summer 2021, Summer 2022

Graduate seminars

  1. Seminars on Software Engineering, Software Analysis, Verification, and Testing

Instruction at University of Passau

Undergraduate courses

  1. Foundations of Computer Science, 5100
    Winter 2010/11
  2. Algorithms and Data Structures, 5200
    Summer 2010
  3. Software Engineering, 5300
    Winter 2009/10, Winter 2012/13, Winter 2013/14, Winter 2014/15
  4. Theoretische Informatik I, 5306
    Winter 2015/16
  5. Theoretische Informatik II, 5308
    Winter 2015/16
  6. Spezifikation und Verifikation von Eingebetteten Systemen, 5463
    Winter 2014/15, Winter 2015/16
  7. Software Engineering Praktikum, 5500
    Summer 2014

Graduate courses

  1. Software Analysis, 5840
    Winter 2009/10, Winter 2011/12
  2. Software Verification, 5843
    Winter 2012/13, Winter 2013/14, Winter 2014/15, Winter 2015/16
  3. Object-Oriented Programming, 5620
    Summer 2010
  4. Principles of Compiler Design, 5790
    Summer 2012, Summer 2013, Summer 2014
  5. Academic and Scientific Methods, 5844
    Summer 2012, Summer 2014

Graduate seminars

  1. Seminar Seminar Entwurf und Analyse von Softwaresystemen, 5846/5847
    Winter 2009/10, Winter 2010/11, Winter 2011/12, Summer 2012, Winter 2013/14, Summer 2014, Winter 2014/15, Winter 2015/16
  2. Seminar Software Testing and Analysis, 5848
    Summer 2010, Winter 2012/13

Events for High-School Students

  1. Sommercamp Informatik, 5900
    Summer 2010, Summer 2011, Summer 2012, Summer 2013, Summer 2014, Summer 2015

Instruction at SFU

Undergraduate courses

  1. Principles of Compiler Design, CMPT 379
    Spring 2008, Spring 2009
  2. Software Engineering II, CMPT 475
    Spring 2007, Spring 2008, Fall 2008

Graduate courses

  1. Software Engineering, CMPT 745
    Fall 2007, Fall 2008
  2. Special Topics in CS - Program Analysis, CMPT 880
    Spring 2007

Graduate seminars

  1. Software Verification, CMPT 894
    Spring 2008, Spring 2009

Teaching Assistant at EPFL and BTU

Undergraduate courses

  1. Theoretical Computer Science, Prof. Henzinger
    Winter 2005/06
  2. Introduction to Computer Science, Prof. Bachmann
    Winter 2002/03
  3. Introduction to Data Structures and Efficient Algorithms, Prof. Heiner
    Winter 2000/01, Winter 1998/99
  4. Introduction to Software Engineering, Prof. Lewerentz
    Summer 2000, Summer 1999
  5. Introduction to Software Engineering (for teachers from high schools), Prof. Lewerentz
    Summer 2000
  6. Introduction to Software Engineering (for engineers from industry), Prof. Lewerentz
    Summer 2002, Summer 1999
  7. Introduction to Software Engineering (for students of engineering), Prof. Lewerentz
    Summer 2001
  8. Computer Science (for students of environmental and resource management), Dr. Rust
    Winter 2000/01, Winter 1999/2000
  9. Software Project, Prof. Lewerentz
    Winter 2002/03, Summer 2002, Winter 2001/02, Summer 2001, Winter 2000/01, Summer 1999

Graduate courses

  1. Computer-Aided Verification, Prof. Henzinger
    Winter 2004/05
  2. Software Engineering I, Prof. Lewerentz
    Winter 2001/02
  3. Software Engineering II, Prof. Lewerentz
    Sommer 2003, Summer 2002, Summer 2001
  4. Software Project Management, Prof. Lewerentz
    Winter 2001/02

Graduate seminars

  1. Thrust in Reliable Software (TRESOR)
    Winter 2004/05, Summer 2005, Winter 2005/06
  2. Complexity and Software
    Winter 2002/03

Advising

Current postdocs

  1. Nian-Ze Lee;
  2. Philipp Wendler;
  3. Stefan Winter;

Current students

  1. Marvin Brieger, PhD program;
  2. Thomas Bunk, PhD program;
  3. Po-Chun Chien, PhD program;
  4. Sudeep Kanav, PhD program;
  5. Matthias Kettl, PhD program;
  6. Martin Spießl, PhD program;
  7. Henrik Wachowitz, PhD program;

PhD thesis supervisor

  1. Matthias Dangl. Witness-based validation of verification results with applications to software-model checking. LMU Munich, 2022.
  2. Thomas Lemberger. Towards cooperative software verification with test generation and formal verification. LMU Munich, 2022.
  3. Karlheinz Friedberger. Efficient software model checking with block-abstraction memoization. LMU Munich, 2022.
  4. Sabine Bauer. Decidability of linear tree constraints for resource analysis of object-oriented programs. LMU Munich, 2019.
  5. Philipp Wendler. Towards practical predicate analysis. University of Passau, 2017.
  6. Stefan Löwe. Effective approaches to abstraction refinement for automatic software verification. University of Passau, 2017.
  7. Mehmet ‍Erkan Keremoglu. Towards scalable software analyisis using combinations and conditions with CPAchecker. Simon Fraser University, 2011.
  8. Grégory Théoduloz. Software verification by combining program analyses of adjustable precision. EPFL, MTC Lab, supervised by Prof. Thomas Henzinger, 2010.

Master’s thesis supervisor

  1. Daniel Baier. Implementation of value analysis over symbolic memory graphs in cpachecker. LMU Munich, 2022.
  2. Martin Pletl. A new spin on verification with symbolic execution: Symbolic execution as formula-based predicate analysis in cpachecker. LMU Munich, 2022.
  3. Maximilian Hailer. New approaches and visualization for verification coverage. LMU Munich, 2022.
  4. Matthias Kettl. Adjustable block analysis: Actor-based creation of block summaries for scaling formal verification. LMU Munich, 2022.
  5. Philipp Waldinger. Concurrent software verification through block-based task partitioning and continuous summary refinement. LMU Munich, 2022.
  6. Moritz Beck. Solver-based analysis of memory safety using separation logic. LMU Munich, 2020.
  7. Alexander Koos. Implementation and evaluation of a framework for canonization and caching of SMT formulae. LMU Munich, 2019.
  8. Stephan Holzner. Design und Implementierung einer parallelen BDD-Bibliothek. LMU Munich, 2019.
  9. Michael Maier. SMT-based verification of ECMAScript programs in CPAchecker. LMU Munich, 2019.
  10. Mirjam Trapp. Heuristics for effective predicate refinement in CPAchecker. LMU Munich, 2019.
  11. Thomas Bunk. LTL software model checking in CPAchecker. LMU Munich, 2019.
  12. Johannes Knaut. Symbolic heap abstraction with automatic refinement. LMU Munich, 2018.
  13. Martin Spiessl. Configurable software verification based on slicing abstractions. LMU Munich, 2018.
  14. Thomas Lemberger. Abstraction refinement for model checking: Program slicing + CEGAR. LMU Munich, 2018.
  15. Thomas Stieglmaier. Augmenting predicate analysis with auxiliary invariants. University of Passau, 2016.
  16. Sebastian Ott. Implementing a termination analysis using configurable software analysis. University of Passau, 2016.
  17. Karlheinz Friedberger. Block-abstraction memoization as an approach to verify recursive procedures. University of Passau, 2015.
  18. Matthias Dangl. Light-weight invariant generation for software verification with CPAchecker. University of Passau, 2013.
  19. Christopher Jahn. Implementation of a CFA and ARG visualization and navigation tool in Java. University of Passau, 2012.
  20. Andreas Stahlbauer. Block-encoding strategies for predicate analysis: An experimental study. University of Passau, 2012.
  21. Peter Häring. A comparative study of software measures as problem-predictors. University of Passau, 2012.
  22. Andra-Maria Babau. Modeling and verification of airport security processes using BPMN and protocol interfaces: A case study. University of Passau, 2011.
  23. Dmitry Balzer. Werkzeugunterstützung für Verstehen und Monitoring von Software-Abhängigkeiten. University of Passau, 2010.
  24. Alexander von Rhein. Verification tasks for software model checking. University of Passau, 2010.
  25. Ashgan Fararooy. Performing static structure analysis using software dependencies. Simon Fraser University, 2010.
  26. Philipp Wendler. Software verification based on adjustable large-block encoding. University of Passau, 2010.
  27. Damien Zufferey. EPFL, MTC Lab, with Prof. Thomas Henzinger, 2009.
  28. Grégory Théoduloz. Integrating shape analysis into the model checker Blast. EPFL, MTC Lab, with Prof. Thomas Henzinger, 2006.
  29. Andreas Noack. BDD-basierte Verifikation von Echtzeitsystemen. BTU Cottbus, with Prof. Claus Lewerentz, 2000.

Bachelor’s thesis supervisor

  1. Moritz Bierwirth. Designing and assessing a benchmark set for fault localization using fault injection. LMU Munich, 2023.
  2. Klara Cimbalnik. Program transformation in CPAchecker: Design and implementation of a source-respecting translation from control-flow automata to c code. LMU Munich, 2022.
  3. Tobias Kleinert. Developing a verifier based on parallel portfolio with CoVeriTeam. LMU Munich, 2022.
  4. Robin Gloster. Cgroups v2 support for BenchExec. LMU Munich, 2022.
  5. Ludwig Glückstadt. Genetic programming in software verification. LMU Munich, 2021.
  6. Simon Antonischki. A cpa for string analysis for java programs in CPAchecker. LMU Munich, 2021.
  7. Penelope Powers. Mutation based automatic program repair in CPAchecker. LMU Munich, 2021.
  8. Korab Zogu. Sv-comp benchmarks for weak memory models. LMU Munich, 2021.
  9. Yun Zhang. Verification witnesses: from llvm to c. LMU Munich, 2021.
  10. Simon Raths. Implementation and evaluation of tbdds in pjbdd. LMU Munich, 2021.
  11. Sebastian Tschoepel. Implementation and evaluation of a simple taint analysis for CPAchecker. LMU Munich, 2021.
  12. Dennis Simon. Shareable benchmarking reports with enhanced filters and dynamic statistics for BenchExec. LMU Munich, 2021.
  13. Martin Zehendner. Software verification with numerical domains in CPAchecker. LMU Munich, 2020.
  14. Sven Umbricht. Converting between acsl annotations and witness invariants. LMU Munich, 2020.
  15. Benedikt Damböck. Implementierung und evaluation von einfacher schleifenabstraktion für das CPAchecker-framework. LMU Munich, 2020.
  16. Sven Massard. Improve analysis of java programs in CPAchecker. LMU Munich, 2020.
  17. Frederic Schönberger. Converting test goals to condition automata. LMU Munich, 2020.
  18. Jakob Selberg. Automatic generation of test harnesses for pointer-based c programs: Implementation of a pointer-tracking analysis and harness-generation engine in the formal verification framework CPAchecker. LMU Munich, 2020.
  19. Yannick Adams. Domain types for predicate analysis in CPAchecker. LMU Munich, 2020.
  20. Vladyslav Kolesnykov. SMT-based model checking of concurrent programs. LMU Munich, 2020.
  21. Radu-Cristian Rusanu. Interval-based optimization for smt solvers. LMU Munich, 2020.
  22. Amena Abdulla. Reale anforderungen für die software-analyse. LMU Munich, 2020.
  23. Simon Lund. Code complexity measures in software engineering: A systematic comparison and evaluation on software-component level. LMU Munich, 2020.
  24. Angelos Kafounis. Fault localization in model checking. implementation and evaluation of fault-localization techniques with distance metrics. LMU Munich, 2020.
  25. Schindar Ali. Test-based fault localization in the context of formal verification: Implementation and evaluation of the tarantula algorithm in cpachecker. LMU Munich, 2020.
  26. Petros Isaakidis. Energy consumption prediction of verification work. LMU Munich, 2020.
  27. Matthias Kettl. Fault localization for formal verification: An implementation and evaluation of algorithms based on error invariants and unsat-cores. LMU Munich, 2020.
  28. Sonja Münchow. A web frontend for visualization of computation steps and their results in cpachecker. LMU Munich, 2020.
  29. Adrian Leimeister. A language server and ide plugin for CPAchecker. LMU Munich, 2020.
  30. Michael Obermeier. Extending the framework JavaSMT with the SMT solver Yices2. LMU Munich, 2020.
  31. Alexander Ried. Design and implementation of a cluster-based approach for software verification. LMU Munich, 2020.
  32. Maximilian Hailer. Measuring and optimizing energy consumption of verification work on clusters. LMU Munich, 2019.
  33. Daniel Baier. Integration des SMT-Solvers Boolector in das Framework JavaSMT und Evaluation mit CPAchecker. LMU Munich, 2019.
  34. Laura Bschor. Modern architecture and improved UI for tables of BenchExec. LMU Munich, 2019.
  35. Maximilian Wiesholler. Correctness witness validation using predicate analysis. LMU Munich, 2019.
  36. Krutav Shah. Counterexample-guided abstraction refinement for interval domain. LMU Munich, 2019.
  37. Raphael Hagl. Hybrid testcase generation with CPAchecker. LMU Munich, 2019.
  38. Andrea Kreppel. Implementation and evaluation of backwards analyses in the software-verification framework CPAchecker. LMU Munich, 2019.
  39. Matthias Gerlach. Newton refinement as alternative to Craig interpolation in CPAchecker. LMU Munich, 2018.
  40. Flutura Estler. Heuristics-based selection of verification configurations. LMU Munich, 2018.
  41. Balthasar Schuess. Flexible online job scheduling in a multi-user environment. LMU Munich, 2018.
  42. Dominik Friedrich. Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker. LMU Munich, 2018.
  43. Moritz Buhl. Application of software verification to OpenBSD network modules. LMU Munich, 2018.
  44. Nicholas Reyes. Integrating a witness store into a distributed verification system. LMU Munich, 2018.
  45. Dominik Pastau. Implementation of a generic cloud-based file-storage solution and its integration into a web-based distributed verification system. LMU Munich, 2018.
  46. Karam Shabita. String analysis for Java programs in CPAchecker. LMU Munich, 2018.
  47. Evgeny Dunaev. Entwurf und Implementierung einer Abstraktionsschicht für Zuweisungs-basierte Analysen. LMU Munich, 2017.
  48. Deyan Ivanov. Interactive visualization of verification results from CPAchecker with D3. LMU Munich, 2017.
  49. Nils Steinger. Measuring, visualizing, and optimizing the energy consumption of computer clusters. University of Passau, 2017.
  50. Gernot Zoerneck. Implementing PDR in CPAchecker. University of Passau, 2017.
  51. Stefan Weinzierl. Configurable pointer-alias analysis in CPAchecker. University of Passau, 2016.
  52. Maximilian Syri. Verification of concurrent programs by CFA sequentialization. University of Passau, 2016.
  53. Stephan Lukasczyk. Unbounded heap support for CPAchecker’s predicate analysis using SMT arrays. University of Passau, 2016.
  54. Magdalena Murr. Towards understandable CPAchecker counterexamples. University of Passau, 2016.
  55. Thomas Lemberger. Efficient symbolic execution using CEGAR over two abstract domains. University of Passau, 2015.
  56. Sebastian Ott. VerifierCloud: Implementierung eines web-service zur software-verifikation. University of Passau, 2014.
  57. Thomas Stieglmaier. Octagon-based software verification with CPAchecker. University of Passau, 2014.
  58. Georg Dresler. A google-app-engine implementation for CPAchecker. University of Passau, 2014.
  59. Matthias Dittrich. Bit-precise predicate analysis with CPAchecker. University of Passau, 2013.
  60. Alexander Driemeyer. Software-verifikation von java-programmen in cpachecker. University of Passau, 2012.
  61. Karlheinz Friedberger. Ein typbasierter Ansatz zur Kombination verschiedener Verifikationstechniken. University of Passau, 2012.

Internship students

  1. Emanuele De Angelis (from University of Chieti-Pescara), Uni Passau, 2013;
  2. Przemyslaw Daca (from TU Denmark), Uni Passau, 2011;
  3. Philipp Wendler (from Uni Passau), SFU, 2009;
  4. Michael Tautschnig (from TU Darmstadt), SFU, 2008;
  5. Andreas Holzer (from TU Darmstadt), SFU, 2008;
  6. Alberto Griggio (from Uni Trento), SFU, 2008;
  7. Damien Zufferey (from EPFL), SFU, 2007;
  8. Sudhanshu Narang (from IIT Delhi), SFU, 2007;
  9. Rajhans Samdani (from IIT Bombay), EPFL, 2006;
  10. Nitesh Kumar (from IIT Kanpur), EPFL, 2005

PhD thesis referee

  1. Nian-Ze Lee; National Taiwan University, 2021
  2. Marie-Christine Jakobs, University of Paderborn, 2016
  3. Daniel Dietsch, University of Freiburg, 2016
  4. George Karpenkov, University of Grenoble, 2016
  5. Evren Ermis, University of Freiburg, 2014
  6. Jiri Slaby, Masaryk University, 2014
  7. Andreas Holzer, TU Vienna, 2013

PhD thesis defense chair

  1. Jan Seedorf, Uni Passau, 2013
  2. Roozbeh Farahbod, SFU, 2009

PhD depth examination chair

  1. Brian Fraser, SFU, 2007

MSc thesis referee

  1. Siegfried Rasthofer, Uni Passau, 2013
  2. Stephan Huber, Uni Passau, 2012
  3. Hendrik Speidel, Uni Passau, 2011
  4. Kathrin Hanauer, Uni Passau, 2010
  5. George Ma, SFU, 2007

MSc thesis defence examiner

  1. Wolfgang Haas, SFU, 2007;
  2. George Ma, SFU, 2007

MSc thesis defense chair

  1. Kaiyan Jin, SFU, 2009;
  2. Edward Glen, SFU, 2007;
  3. Majid Bagheri, SFU, 2007;
  4. Chiyoko Kawano, SFU, 2006

Departmental and University Committees

  1. Chair Prüfungsausschuss Informatik IfI, LMU Munich, since 2019
  2. Chair of the Department of Computer Science, LMU Munich, 2020–2022
  3. Chair Berufungskommission W3 “Programmierung and AI”, LMU Munich, 2021–2022
  4. Chair Berufungskommission W3 “Theoretische Informatik (2)”, LMU Munich, 2021–2022
  5. Berufungskommission W3 “Technology-Enhanced Learning”, LMU Munich, 2019
  6. Berufungskommission W1 “Medieninformatik”, LMU Munich, 2019
  7. Chair Berufungskommission W3 “Theoretische Informatik”, LMU Munich, 2018–2019
  8. Berufungskommission W1 “Software Engineering”, LMU Munich, 2018–2019
  9. Prüfungsausschuss IfI, LMU Munich, 2016–2019
  10. Promotionsausschuss FIM, Uni Passau, 2015–2017
  11. Faculty Council, Uni Passau, 2013–2015
  12. Studiengangsverantwortlicher MSc Informatik, Uni Passau, 2015–2016
  13. Studienberater Lehramt Informatik, Uni Passau, 2011–2016
  14. Promotionsausschuss FIM, Uni Passau, 2013–2015
  15. Berufungskommission W3 “Theoretische Informatik”, Uni Passau, 2014–2015
  16. Berufungskommission W3 “Betriebliche Informationssysteme”, Uni Passau, 2014
  17. Chair Berufungskommission W3 “Complex-Systems Engineering”, Uni Passau, 2012
  18. Berufungskommission W3 “Embedded Systems”, Uni Passau, 2012
  19. Promotionsausschuss FIM, Uni Passau, 2010–2013
  20. Berufungskommission W2 “Medieninformatik”, Uni Passau, 2011
  21. Berufungskommission W3 “Bildverarbeitung”, Uni Passau, 2009–2011
  22. Hardware and Capital Resources Committee, SFU, 2008–2009
  23. Faculty Recruiting Committee, SFU, 2007–2008
  24. Faculty Council, BTU Cottbus, 1998–2000
  25. President of the CS Students’ Organization, BTU Cottbus, 1997–1998
© Dirk Beyer
This document was translated from LATEX by HEVEA.