Short Curriculum Vitae for Sabine Glesner 

---

Degrees

• Habilitation, Universität Karlsruhe, Fakultät für Informatik, Mai 2005
  Lehrbefugnis für das Fach Informatik
• PhD (Dr. rer. nat.), "Mit Auszeichnung", Universität Karlsruhe, Fakultät für Informatik, February 1999
• Diplom in Informatik ("Mit Auszeichnung bestanden"), Technische Hochschule Darmstadt, March 1996
• Master of Science in Computer Science, University of California, Berkeley, December 1994

Awards

• Preis des Fördervereins "Forschungszentrum Informatik" for one of the two best dissertations in the Computer Science Department, University of Karlsruhe, 1999
• Fulbright Grant (August 1993 - December 1994)
• Scholarship of the Studienstiftung des deutschen Volkes (1991 - 1996)
• Member of the Siemens Internationaler Studentenkreis / Doktorandenkreis

Research Grants and Projects

• Member in the "Margarete von Wrangell-Habilitationsprogramm", sponsored by the state of Baden-Wuerttemberg (Germany)
• Correct and Optimizing Compilers for Modern Processor Architectures: Research grant in the "Eliteförderprogramm für Postdoktoranden der Landesstiftung Baden-Württemberg", sponsored with 69.000 Euro.
• Research grant within the DFG Aktionsplan Informatik (part of the Emmy Noether-Programm) starting 2004
  Titel des Projekts: Verifikation und Optimierung bei der Übersetzung höherer Programmiersprachen.
  Förderung zum Aufbau einer eigenen Arbeitsgruppe (u.a. zwei Mitarbeiterstellen)

Research Interests

• Compiler Verification, especially by formal correctness proofs within the Isabelle/HOL system
• Compiler for Embedded Systems, with particular emphasis on formally correct and optimizing code generation
• Semantics of programming languages
• Logics in Artificial Intelligence, especially Bayesian networks, and automated theorem provers

Teaching

• Course (Vorlesung) on Programming Languages (Höhere Programmiersprachen), winter term 2004/05
• Course (Vorlesung) on Advanced Compiler Construction (Ausgewählte Kapitel aus dem Übersetzerbau), summer term 2004
• Course (Vorlesung) on Programming Languages (Höhere Programmiersprachen), winter term 2003/04
• Course (Vorlesung) on Advanced Compiler Construction (Ausgewählte Kapitel aus dem Übersetzerbau), summer term 2003
• Seminar on Intermediate Representations and Code Generation (Zwischensprachen und Codegenerierung), summer term 2003
• Course (Vorlesung) on Programming Languages (Höhere Programmiersprachen), winter term 2002/2003
• Course (Vorlesung) on Advanced Compiler Construction (Ausgewählte Kapitel aus dem Übersetzerbau), summer term 2002
• Exercises (Übungen) for the course on Compiler Construction (Übersetzerbau), winter term 2001/02.
• Proseminar on XML: "XML-Eine einheitliche Sprache nicht nur im Web", winter term 2001/02
• Proseminar on XML: "XML-Die neue Sprache nicht nur im Web", winter term 2000/01
• Proseminar on XML: "XML-Die neue Sprache nicht nur im Web", winter term 1999/2000
• Proseminar on Program Analysis: "Verfahren zur Programmanalyse", summer term 1999
• Proseminar on randomized algorithms: "Zufallsgesteuerte Algorithmen", winter term 1996/97

Advised Students

Promotionen (PhD Theses)

• Jan Olaf Blech: PhD Thesis on the Verification of Compiler Optimizations, has started in April 2004.
• Lars Gesellensetter: PhD Thesis on Global Machine-dependent Compiler Optimizations, starting July 2004.

Diplomarbeiten (Master's Theses)

• Elyasin Shaladi: Diplomarbeit "Verifikation von Schleifentransformationen in Compilern", Fakultät für Informatik, Universität Karlsruhe, laufende Arbeit.
• Andreas Humbert: Diplomarbeit "Eine strukturell operationale Semantik für SSA-Sprachen", Fakultät für Informatik, Universität Karlsruhe, laufende Arbeit.
• Horia Barca: Diplomarbeit "Eine formale Semantik für den Pi-Kalkül", Fakultät für Informatik, Universität Karlsruhe, laufende Arbeit.
• Hannes Jakschitsch: Diplomarbeit "Befehlsauswahl auf SSA-Graphen", Fakultät für Informatik, Universität Karlsruhe, November 2004.
• Jan Olaf Blech: Diplomarbeit "Eine formale Semantik für SSA-Zwischensprachen in Isabelle/HOL", Fakultät für Informatik, Universität Karlsruhe, März 2004.
• Sebastian Hack: Diplomarbeit "Graphersetzung für Optimierungen in der Codeerzeugung", Fakultät für Informatik, Universität Karlsruhe, Dezember 2003.
• Hannah Schröter: Diplomarbeit "Codegenerierung für digitale Signalprozessoren: Erweiterung eines Codegeneratorgenerators basierend auf Graphersetzungsmethoden", Fakultät für Informatik, Universität Karlsruhe, Februar 2003.

Studienarbeiten (Term Projects)

• Andreas Humbert: Studienarbeit "Entwurf und Implementierung einer XML-Schnittstelle für SSA-Sprachen in Übersetzern", Fakultät für Informatik, Universität Karlsruhe, Juni 2005.
• Max Schroeder: Studienarbeit "Checker für Konstantenpropagierung in Compilern", Fakultät für Informatik, Universität Karlsruhe, Juni 2005.
• Johannes Leitner: Studienarbeit "Koalgebraische Methoden in der maschinellen Verifikation von optimierenden Programmtransformationen", Fakultät für Informatik, Universität Karlsruhe, Februar 2005.
• Steffen Mülling: Studienarbeit "Maschinelle Verifikation der Codeerzeugung für VLIW-Prozessoren", Fakultät für Informatik, Universität Karlsruhe, 2005.
• Robert Hartmann: Studienarbeit "Evaluierung graphersetzungsbasierter Optimierungen in Compiler-Backends", Fakultät für Informatik, Universität Karlsruhe, 2005.
• Karsten Sperling: Studienarbeit "Verifikation unimodularer Schleifentransformationen", Fakultät für Informatik, Universität Karlsruhe, Dezember 2004.
• Denise Dudek: Studienarbeit "Maschinelle Verifikation der Eliminierung toten Codes in SSA-Darstellungen", Fakultät für Informatik, Universität Karlsruhe, 2005.
• Simone Forster: Studienarbeit "Formale Verifikation der syntaktischen Analyse des GCC-Compilers in Isabelle/HOL", Fakultät für Informatik, Universität Karlsruhe, Februar 2005.
• Andreas Arnold: Studienarbeit "Codeerzeugung aus Firm mit dem lcc-Backend", Fakultät für Informatik, Universität Karlsruhe, November 2004.
• Matthias Jäger: Studienarbeit "Generierung von .NET IL Assembler aus Firm", Fakultät für Informatik, Universität Karlsruhe, März 2003.
• Jan Olaf Blech: Studienarbeit "Spezifikation und maschinelle Verifikation von Konstantenfaltung in Übersetzern", Fakultät für Informatik, Universität Karlsruhe, Mai 2003.
• Rubino Geiß: Studienarbeit "The Sherlock-System - A Prototype for Many-Sorted Natural Semantics", Fakultät für Informatik, Universität Karlsruhe, Dezember 1998.