Ich bin derzeit Doktorand am I11, wo ich das Projekt [mc]square leite. Bei [mc]square handelt es sich um einem Model-Checker für Binärcode auf verschiedenen Mikrocontroller-Plattformen. Hierbei konzentriere ich mich vor allem auf die Entwicklung von statischen Analysen zur Fehlererkennung sowie zur Abstraktion. Bevor ich zum Lehrstuhl Informatik 11 an die RWTH Aachen gewechselt bin, habe ich Informatik an der Christian-Albrechts-Universität zu Kiel studiert und war am NICTA, wo ich an Goanna, einem Tool zur statischen Analyse von C/C++ Code gearbeitet habe.

Mein Lebenslauf ist hier erhältlich.

• 22.03.2011: Das Papier Existential Quantification as Incremental SAT, welches ich gemeinsam mit Andy King und Jael Kriener geschrieben habe, wurde auf CAV'11 akzeptiert.
• 11.03.2011: Von April bis Juni werde ich die Gruppe von Kim G. Larsen in Aalborg besuchen, Kontaktaufnahme daher bitte per E-Mail.
• 10.02.2011: Gemeinsam mit Marco Roveri (FBK-IRST, Trento) und Hendrik Tews (TU Dresden) werde ich den 6th International Workshop on Systems Software Verification (SSV'11) organisieren.
• 09.02.2011: Das Papier Approximate Quantifier Elimination for Propositional Boolean Formulae, welches ich gemeinsam mit Andy King geschrieben habe, wurde auf NFM'11 akzeptiert.
• 07.12.2010: Das Papier Transfer Function Synthesis without Quantifier Elimination, welches ich gemeinsam mit Andy King geschrieben habe, wurde auf ESOP'11 akzeptiert.
• 28/10/2010: Gemeinsam mit Thomas Reinbacher, Martin Horauer, Andreas Steininger und Stefan Kowalewski, habe ich für unseren Beitrag zur MEMICS'10 einen mit 10.000 CZK dotierten Best Paper Award erhalten.
• 08/06/2010: Das Papier Range Analysis of Microcontroller Code using Bit-Level Congruences, welches ich gemeinsam mit Andy King und Stefan Kowalewski geschrieben habe, wurde auf FMICS'10 akzeptiert.
• 04/05/2010: Das Papier Automatic Abstraction for Intervals using Boolean Formulae, welches ich gemeinsam mit Andy King geschrieben habe, wurde auf SAS'10 akzeptiert.

• Lokaler Organisator des 4th International Workshop on Systems Software Verification (SSV 2009) in Aachen, Deutschland
• Mitglied des Programmkommitees des 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) in Antwerpen, Belgien

• Statische Analyse von Mikrocontroller Software
• Abstrakte Interpretation
• Pointer Analyse
• Formale Verifikation
• Software Model-Checking

Zusammenfassend beschäftige ich mich mit der Fragestellung, wie man Prinzipien der theoretischen Informatik anwenden kann, um Low-Level Programme zu verifizieren. Hierbei interessiert mich insbesondere die Anwendung von SAT und SMT Solvern und deren Zusammenspiel mit abstrakter Interpretation. Bei Interesse an diesem Thema empfehle ich, einen Blick auf mein SAS'10 Papier oder mein ESOP'11 Papier zu werfen, welche einen guten Überblick darüber geben, welche Präzision sich mit SAT-basierter abstrakter Interpretation erreichen läßt.

Wir haben stets eine größere Anzahl von offenen Themen für Abschlussarbeiten, auch über die auf dieser Seite gelisteten Themen hinaus. Wenn Interesse daran besteht, die eigene Abschlussarbeit im Bereich der Software-Verifikation für eingebettete Systeme zu schreiben, dann kontaktiert mich bitte per E-Mail.

• Offen
• Laufend
  • Na Bai (Diplom): Datenflussanalyse für Speicherprogrammierbare Steuerungen
  • Mustafa Karafil (Diplom): Analyse von indirektem Kontrollfluss
• Abgeschlossen
  • Sebastian Biallas (Diplom): Gegenbeispiel-geleitete Abstraktionsverfeinerung für speicherprogrammierbare Steuerungen
  • Frank Birbacher (Diplom): Relationale Analyse von SPSen mittels Kongruenzen
  • Lucas Brutschy (B.Sc.): Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und SMT-Solving
  • Jörg Toborg (Diplom): Statische Analyse für den Renesas R8C/23 Tiny

Eine detaillierte Übersicht über meine Veröffentlichungen findet sich hier.

<BIBTEX: file=publikationen style=I11 sort=timestamp filter=brauer referenz=journal>

<BIBTEX: file=publikationen style=I11 sort=timestamp filter=Brauer referenz=conference>

• Sommersemester 2010
  • Seminar: Programmanalyse
• Wintersemester 2009/2010
  • Formale Methoden für eingebettete Systeme (Vorlesung)
  • Verifikation und Programmanalyse (Seminar)
• Sommersemester 2009
  • Anwendung formaler Verifikationsmethoden auf eingebettete Systeme (Seminar)
• Wintersemester 2008/2009
  • Statische Analyse von Software für eingebettete Systeme (Seminar)