Teaching Acitivities
Lectures
- Summer 2021: Quantitative Verification
- Winter 2020/21: Verification of Digital Circuits
- Summer 2020: Quantitative Verification
- Winter 2019/20: Verification of Digital Circuits
- Summer 2019: Quantitative Verification
- Winter 2018/19: Verification of Digital Circuits (together with Prof. Scholl)
- Summer 2018: Quantitative Verification
- Winter 2017/18: Technische Informatik
- Summer 2017: Computer Architecture
- Winter 2016/17: Technische Informatik (together with Dr. Schubert)
- Winter 2016/17: Symbolic Verification (block course at the Chinese Academy of Sciences in Beijing, China)
- Summer 2016: Verification of Digital Circuits
- Winter 2015/16: Formal Engineering of Digital and Hybrid Systems (at Saarland University, Saarbrücken)
- Summer 2015: Cyber-Physical Systems II: Hybrid Models (together with Prof. Becker)
- Winter 2014/15: Verification of Embedded Systems (together with Prof. Scholl)
- Summer 2014: Cyber-Physical Systems II: Hybrid Models
- Winter 2013/14: Verifikation eingebetteter Systeme
- since Winter 2013/14: Verifikation eingebetteter Systeme als Online-Vorlesung im berufsbegleitenden Studiengang Master in Intelligent Embedded Microsystems (IEMS)
- Summer 2013: Verifikation probabilistischer Systeme
- Winter 2012/13: Verifikation eingebetteter Systeme (together with Dr. Marin)
- Summer 2012: Rechnerarchitektur
- Winter 2011/12: Verifikation probabilistischer und hybrider Systeme
- Winter 2010/11: Systeme I: Betriebssysteme
- Summer 2009: Einführung in die effiziente Softwareentwicklung mit C++
Seminar Courses
- Winter 2015/16: Quantified Boolean Formulas: Algorithms & Applications (at Saarland University, Saarbrücken)
- Summer 2015: (Dependency) Quantified Boolean Formulas (together with Prof. Becker)
- Summer 2011: Techniques for the Verification of Probabilistic and Timed Automata (together with Prof. Becker)
- Summer 2010: Model Checking – Probabilistische und Echtzeitaspekte (together with Prof. Becker)
- Winter 2008/09: Satisfiability modulo Theories (together with Prof. Becker and others)
- (several times) Computer-Aided Engineering (together with Prof. Becker)
Academic Theses and Projects
Diploma
- Kelley Strampp: "Symbolische Berechnung von Bisimulationen", 2006
- Natalia Kalinnik: "Kompositionalität und Bounded Model Checking", 2006
- Alexander Kortus: "Bounded Model Checking für stochastische Systeme", 2007
- Eric Nyaben: "Model Checking für stochastische Systeme mit Black Boxes", 2008
- Bettina Braitling: "Bounded Model Checking auf stochastischen Systemen" (Continuation of Alexander Kortus' work), 2008
Master of Science
- Leonore Winterer: "Über die Verifikation maschinell gelernter Controller", 2014
- Marius Hollinger: "Solving DQBF by Skolemization", 2016 (at Saarland University, Saarbrücken)
- Jennifer Nist: "Improving Dependency Elimination for DQBF", 2018
Bachelor of Science
- Markus Fuchs: "Visualisierung von SAT-Algorithmen", 2007
- Tobias Seufert: "Model Checking für Markow-Reward-Modelle mit beschränkten Resourcen", 2011
- Georg Thombansen: "Minimale kritische Teilsysteme für Markow-Entscheidungsprozesse", 2012
- Madeleine Pairan: "Gegenbeispiele für Expected-Reward-Eigenschaften von Markow-Modellen mit kontinuierlicher Zeit", 2013
- Jennifer Nist: "Vorverarbeitung für DQBF", 2015
- David Zschocke: "Calculation of Skolem Functions for DQBF", 2015
- Jens Heinen: "Unidex: Ein Vergleichstool für Informatikfakultäten", 2016 (at Saarland University, Saarbrücken)
- Julika Feldbusch: "Skolem-Funktionen für DQBF-Solver und -Präprozessor", 2019/20
Student Projects
- Christoph Löffler: "xGen - ein Webportal zur Generierung von Übungsblättern"
- Georges Morbé: "Ein semi-symbolischer Algorithmus für Paritätsspiele"
- Alexander Kortus: "Probabilistisches Model-Checking mit exakter Arithmetik"
- Andreas Spilla, Daniel Frey, and Eduard Skaley: "xGen2 - ein Portal zur Generierung von Übungsblättern"
- Jennifer Modes: "Implementierung eines stochastischen SAT-Solvers"
- Jan Hättig: "BDD-basierte Berechnung von Gegenbeispielen für Markow-Ketten"
- Tobias Seufert: "Analyse von Erreichbarkeitswahrscheinlichkeiten in unvollständigen Netzwerken von Markow-Entscheidungsprozessen"
- Mareike Höchner: "Lernen von Automatenmodellen aus Spike-Recordings"
- Uwe Waldvogel: "Semantische Gattererkennung und Detektion äquivalenter Gatter"
