HOME | ENGLISH | IMPRESSUM | KIT

Dr. rer. nat. Andreas Lochbihler

photo

Kontakt

Email: Loading...

Seit Januar 2013 bin ich als Postdoc an der ETH Zurich an David Basins Lehrstuhl. Zur neuen Homepage.

Arbeitsgebiete

Formale Semantik
Im Rahmen meiner Dissertation arbeitete ich an einem formalen, maschinengeprüften Modell für Java einschließlich Threads, sowohl für Java-Quelltext als auch für Bytecode. Das Modell im Theorembeweiser Isabelle/HOL basiert auf der Sprache Jinja von T. Nipkow und G. Klein und deckt inzwischen alle Sprach- und Synchronisationsprimitive für Threads und Nebenläufigkeit sowie das Java-Speichermodell ab. Die Semantiken für Quell- und Bytecode sind ausführbar und bewiesenermaßen typsicher. Weiterhin gehöhrt ein formalisierter, verifizierter und ausführbarer Compiler, der Quelltextprogramme in verhaltensäquivalente Bytecode-Programme übersetzt. Das Modell ist im Archive of Formal Proofs unter dem Titel Jinja with Threads erschienen und zum Download erhältlich.

Dazu wurde das Konvertierungstool Java2Jinja als Eclipse-Plugin entwickelt, das Java-Programme in die Eingabesyntax von JinjaThreads konvertiert.

Theorembeweiser
Code-Generatoren erlauben, automatisch formale Modelle in ausführbare Prototypen umzuwandeln. In diesem Bereich beschäftige ich mich vor allem damit, wie sich Formalisierungen aus dem Theorembeweiser Isabelle/HOL einfach in effiziente Prototypen verwandeln lassen. Ein Schwerpunkt ist dabei der automatische Einsatz effizienter Datenstrukturen.

Programmanalyse
Die statische Programmanalyse Slicing ermittelt, auf welchen Wegen verschiedene Teile eines Programms sich beeinflussen können; dies lässt sich für Informationsflusskontrolle nutzen. Um die Präzision der und Information über die gefundenen Beeinflussungen zu erhöhen, entwickelte ich im Rahmen meiner Diplomarbeit temporale Pfadbedingungen. Diese erlauben es, mit einem Model Checker ganze Programmsequenzen automatisch zu generieren, für die ein entsprechender Informationsfluss auftritt.

Dabei interessiere ich mich auch dafür, wie sichergestellt werden kann, dass die Analysen selbst korrekt und fehlerfrei sind. Dazu arbeite ich an ausführbaren Prototypen von Formalisierungen der Algorithmen, die bereits verifiziert wurden.

Veröffentlichungen

2014

2013

2012

2011

2010

2009

2008

2007

2006

Vorträge & Poster

Gutachtertätigkeiten

  • Zeitschriften: Computer Languages, Systems & Structures; Fundamenta Informaticae; Journal of Automated Reasoning
  • Konferenzen: FSTTCS 2011, ESOP 2012, EMSOFT 2012

Lehre

Projekte

Betreute Studien- und Abschlussarbeiten

abgeschlossen