====== Dr. rer. nat. Jörg Brauer ====== ~~NOTOC~~ ~~NOCACHE~~ ===== Kontakt ===== {| |- ||{{:lehrstuhl:mitarbeiter:brauer.jpg|}} || Wissenschaftlicher Mitarbeiter\\ \\ Tel. +49 241 80 21156\\ Fax +49 241 80 22150\\ \\ Email: brauer[at]embedded[dot]rwth-aachen[dot]de\\ \\ Adresse: Ahornstr. 55, 52074 Aachen, Germany\\ Büro: Raum 2325 (Gebäude H)\\ \\ **Sprechstunde: ** nach Vereinbarung |} \\ \\ ===== Über mich ===== Ich bin derzeit Doktorand am I11, wo ich das Projekt [[http://www.embedded.rwth-aachen.de/mc_square|[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 [[http://www.nicta.com.au|NICTA]], wo ich an [[http://www.nicta.com.au/research/projects/goanna/|Goanna]], einem Tool zur statischen Analyse von C/C++ Code gearbeitet habe. \\ \\ Mein Lebenslauf ist {{:en:lehrstuhl:mitarbeiter:brauer:cv_brauer.pdf|hier}} erhältlich.\\ ===== Neuigkeiten ===== * 22.03.2011: Das Papier //Existential Quantification as Incremental SAT//, welches ich gemeinsam mit [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] und [[http://www.cs.kent.ac.uk/people/rpg/jek26/|Jael Kriener]] geschrieben habe, wurde auf [[http://www.cs.utah.edu/events/conferences/cav2011/|CAV'11]] akzeptiert. * 11.03.2011: Von April bis Juni werde ich die Gruppe von [[http://www.cs.aau.dk/~kgl/|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 {{:bib:bk11b.pdf|Approximate Quantifier Elimination for Propositional Boolean Formulae}}, welches ich gemeinsam mit [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] geschrieben habe, wurde auf [[http://lars-lab.jpl.nasa.gov/nfm2011/|NFM'11]] akzeptiert. * 07.12.2010: Das Papier {{:bib:bk11.pdf|Transfer Function Synthesis without Quantifier Elimination}}, welches ich gemeinsam mit [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] geschrieben habe, wurde auf [[http://software.imdea.org/~gbarthe/esop11/|ESOP'11]] akzeptiert. * 28/10/2010: Gemeinsam mit [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], [[http://embsys.technikum-wien.at/staff/horauer/index.php|Martin Horauer]], [[http://ti.tuwien.ac.at/ecs/people/steininger|Andreas Steininger]] und [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]], habe ich für unseren Beitrag zur [[http://www.memics.cz/2010/index.php|MEMICS'10]] einen mit 10.000 CZK dotierten Best Paper Award erhalten. * 08/06/2010: Das Papier {{:bib:bkk10.pdf|Range Analysis of Microcontroller Code using Bit-Level Congruences}}, welches ich gemeinsam mit [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] und [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] geschrieben habe, wurde auf [[https://es.fbk.eu/events/fmics2010/index.php|FMICS'10]] akzeptiert. * 04/05/2010: Das Papier {{:bib:bk10.pdf|Automatic Abstraction for Intervals using Boolean Formulae}}, welches ich gemeinsam mit [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] geschrieben habe, wurde auf [[http://sas2010.univ-perp.fr/|SAS'10]] akzeptiert. ===== Aktivitäten ===== * Lokaler Organisator des [[http://ssv09.embedded.rwth-aachen.de|4th International Workshop on Systems Software Verification (SSV 2009)]] in Aachen, Deutschland * Mitglied des Programmkommitees des [[http://es.fbk.eu/events/fmics2010/index.php|15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010)]] in Antwerpen, Belgien ===== Forschungsschwerpunkte ===== * 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 {{:bib:bk10.pdf|mein SAS'10 Papier}} oder {{:bib:bk11.pdf|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. ===== Abschlussarbeiten ===== 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 ===== Publikationen ===== Eine detaillierte Übersicht über meine Veröffentlichungen findet sich [[:en:lehrstuhl:mitarbeiter:brauer:publications|hier]].\\ \\ ==== Journals ==== ==== Begutachtete Konferenzen und Workshops ==== ===== Lehre ===== * Sommersemester 2010 * [[:lehre:sose10:programmanalyse]] * Wintersemester 2009/2010 * [[:lehre:wise0910:formale_methoden]] (Vorlesung) * [[:lehre:wise0910:vup_seminar]] (Seminar) * Sommersemester 2009 * [[http://www-i2.informatik.rwth-aachen.de/i2/?id=279|Anwendung formaler Verifikationsmethoden auf eingebettete Systeme]] (Seminar) * Wintersemester 2008/2009 * [[:lehre:wise0809:seminar_statische_analyse]] (Seminar)