3 Papers accepted at ISoLA'20: "An Interface Theory for Program Verification", "Verification Artifacts in Cooperative Verification", and "Violation Witnesses and Result Validation for Multi-Threaded Programs"
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
  2. Formal Specification and Verification
    Summer 2017, Summer 2018

Graduate courses

  1. Semantics for Programming Languages
    Summer 2019
  2. Testing
    Summer 2018, Summer 2019
  3. Software Analysis and Verification
    Winter 2018/19, Winter 2019/20
  4. Formal Specification and Verification II
    Winter 2017/18

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. Marie-Christine Jakobs;
  2. Philipp Wendler;

Current students

  1. Thomas Bunk, PhD program;
  2. Karlheinz Friedberger, PhD program;
  3. Stephan Holzner, PhD program;
  4. Sudeep Kanav, PhD program;
  5. Thomas Lemberger, PhD program;
  6. Martin Spießl, PhD program;

PhD thesis supervisor

  1. Philipp Wendler. Towards practical predicate analysis. University of Passau, 2017.
  2. Stefan Löwe. Effective approaches to abstraction refinement for automatic software verification. University of Passau, 2017.
  3. Mehmet Erkan Keremoglu. Towards scalable software analyisis using combinations and conditions with CPAchecker. Simon Fraser University, 2011.
  4. Grégory Théoduloz. Software verification by combining program analyses of adjustable precision. EPFL, MTC Lab, with Prof. Thomas Henzinger, 2010.

Master’s thesis supervisor

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

Bachelor’s thesis supervisor

  1. Michael Obermeier. Extending the framework JavaSMT with the SMT solver Yices2. LMU Munich, 2020.
  2. Alexander Ried. Design and implementation of a cluster-based approach for software verification. LMU Munich, 2020.
  3. Maximilian Hailer. Measuring and optimizing energy consumption of verification work on clusters. LMU Munich, 2019.
  4. Daniel Baier. Integration des SMT-Solvers Boolector in das Framework JavaSMT und Evaluation mit CPAchecker. LMU Munich, 2019.
  5. Laura Bschor. Modern architecture and improved UI for tables of BenchExec. LMU Munich, 2019.
  6. Maximilian Wiesholler. Correctness witness validation using predicate analysis. LMU Munich, 2019.
  7. Krutav Shah. Counterexample-guided abstraction refinement for interval domain. LMU Munich, 2019.
  8. Raphael Hagl. Hybrid testcase generation with CPAchecker. LMU Munich, 2019.
  9. Andrea Kreppel. Implementation and evaluation of backwards analyses in the software-verification framework CPAchecker. LMU Munich, 2019.
  10. Matthias Gerlach. Newton refinement as alternative to Craig interpolation in CPAchecker. LMU Munich, 2018.
  11. Flutura Estler. Heuristics-based selection of verification configurations. LMU Munich, 2018.
  12. Balthasar Schuess. Flexible online job scheduling in a multi-user environment. LMU Munich, 2018.
  13. Dominik Friedrich. Konzeption, Umsetzung und Visualisierung von statistischen Daten in CPAchecker. LMU Munich, 2018.
  14. Moritz Buhl. Application of software verification to OpenBSD network modules. LMU Munich, 2018.
  15. Nicholas Reyes. Integrating a witness store into a distributed verification system. LMU Munich, 2018.
  16. Dominik Pastau. Implementation of a generic cloud-based file-storage solution and its integration into a web-based distributed verification system. LMU Munich, 2018.
  17. Karam Shabita. String analysis for Java programs in CPAchecker. LMU Munich, 2018.
  18. Evgeny Dunaev. Entwurf und Implementierung einer Abstraktionsschicht für Zuweisungs-basierte Analysen. LMU Munich, 2017.
  19. Deyan Ivanov. Interactive visualization of verification results from CPAchecker with D3. LMU Munich, 2017.
  20. Nils Steinger. Measuring, visualizing, and optimizing the energy consumption of computer clusters. University of Passau, 2017.
  21. Gernot Zoerneck. Implementing PDR in CPAchecker. University of Passau, 2017.
  22. Stefan Weinzierl. Configurable pointer-alias analysis in CPAchecker. University of Passau, 2016.
  23. Maximilian Syri. Verification of concurrent programs by CFA sequentialization. University of Passau, 2016.
  24. Stephan Lukasczyk. Unbounded heap support for CPAchecker’s predicate analysis using SMT arrays. University of Passau, 2016.
  25. Magdalena Murr. Towards understandable CPAchecker counterexamples. University of Passau, 2016.
  26. Thomas Lemberger. Efficient symbolic execution using CEGAR over two abstract domains. University of Passau, 2015.
  27. Sebastian Ott. VerifierCloud: Implementierung eines web-service zur software-verifikation. University of Passau, 2014.
  28. Thomas Stieglmaier. Octagon-based software verification with CPAchecker. University of Passau, 2014.
  29. Georg Dresler. A google-app-engine implementation for CPAchecker. University of Passau, 2014.
  30. Matthias Dittrich. Bit-precise predicate analysis with CPAchecker. University of Passau, 2013.
  31. Alexander Driemeyer. Software-verifikation von java-programmen in cpachecker. University of Passau, 2012.
  32. 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. Jiri Slaby, Masaryk University, 2014
  2. 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. Berufungskommission W3 “Technology-Enhanced Learning”, LMU Munich, 2019
  3. Berufungskommission W1 “Medieninformatik”, LMU Munich, 2019
  4. Chair Berufungskommission W3 “Theoretische Informatik”, LMU Munich, 2018–2019
  5. Berufungskommission W1 “Software Engineering”, LMU Munich, 2018–2019
  6. Prüfungsausschuss IfI, LMU Munich, 2016–2019
  7. Promotionsausschuss FIM, Uni Passau, 2015–2017
  8. Faculty Council, Uni Passau, 2013–2015
  9. Studiengangsverantwortlicher MSc Informatik, Uni Passau, 2015–2016
  10. Studienberater Lehramt Informatik, Uni Passau, 2011–2016
  11. Promotionsausschuss FIM, Uni Passau, 2013–2015
  12. Berufungskommission W3 “Theoretische Informatik”, Uni Passau, 2014–2015
  13. Berufungskommission W3 “Betriebliche Informationssysteme”, Uni Passau, 2014
  14. Chair Berufungskommission W3 “Complex-Systems Engineering”, Uni Passau, 2012
  15. Berufungskommission W3 “Embedded Systems”, Uni Passau, 2012
  16. Promotionsausschuss FIM, Uni Passau, 2010–2013
  17. Berufungskommission W2 “Medieninformatik”, Uni Passau, 2011
  18. Berufungskommission W3 “Bildverarbeitung”, Uni Passau, 2009–2011
  19. Hardware and Capital Resources Committee, SFU, 2008–2009
  20. Faculty Recruiting Committee, SFU, 2007–2008
  21. Faculty Council, BTU Cottbus, 1998–2000
  22. President of the CS Students’ Organization, BTU Cottbus, 1997–1998
© Dirk Beyer
This document was translated from LATEX by HEVEA.