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
-
Making the Java Memory Model Safe
ACM Transactions on Programming Languages and Systems 2014, pp. 12:1--12:65 : A. Lochbihler
2013
-
Light-weight Containers
Archive of Formal Proofs April 2013 : A. Lochbihler -
Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler
Ausgezeichnete Informatikdissertationen 2012 2013, pp. 211 - 221 : A. Lochbihler -
Light-weight containers for Isabelle: efficient, extensible, nestable
Interactive Theorem Proving 2013, pp. 116--132 (ITP 2013) : A. Lochbihler
2012
-
The Java Memory Model is Type Safe
December 2012 : A. Lochbihler -
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
July 2012 : A. Lochbihler -
Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation
Programming Languages and Systems March 2012, pp. 497--517 (ESOP 2012) : A. Lochbihler
2011
-
A Unified, Machine-Checked Formalisation of Java and the Java Memory Model
December 2011 : A. Lochbihler -
Animating the Formalised Semantics of a Java-like Language
Interactive Theorem Proving 2011, pp. 216--232 (ITP 2011) : A. Lochbihler, L. Bulwahn
2010
-
The Isabelle Collections Framework
July 2010, pp. 339--354 (ITP 2010) : P. Lammich, A. Lochbihler -
Gateway Decompositions for Constrained Reachability Problems
Proceedings of the 9th International Symposium on Experimental Algorithms May 2010, pp. 449--461 (SEA 2010) : B. Katz, M. Krug, A. Lochbihler, I. Rutter, G. Snelting, D. Wagner -
Verifying a Compiler for Java Threads
European Symposium on Programming (ESOP'10) March 2010, pp. 427--447 (ESOP 2010) : A. Lochbihler -
Coinductive
Archive of Formal Proofs February 2010 : A. Lochbihler
2009
-
Formalising FinFuns - Generating Code for Functions as Data from
Isabelle/HOL
Proceedings of the 22nd International Conference of Theorem Proving in Higher Order Logics August 2009, pp. 310--326 (TPHOLs 2009) : A. Lochbihler -
On Temporal Path Conditions in Dependence Graphs
Journal of Automated Software Engineering June 2009, pp. 263--290 (JASE) : A. Lochbihler, G. Snelting -
Code Generation for Functions as Data
Archive of Formal Proofs May 2009 : A. Lochbihler
2008
-
Formalizing a Framework for Dynamic Slicing of Program Dependence
Graphs in Isabelle/HOL
Proceedings of the 21st International Conference of Theorem Proving in Higher Order Logics August 2008, pp. 294--309 (TPHOLS 2008) : D. Wasserrab, A. Lochbihler -
The Computational Complexity of Evolutionarily Stable Strategies
International Journal of Game Theory April 2008, pp. 93--113 : K. Etessami, A. Lochbihler -
Type Safe Nondeterminism - A Formal Semantics of Java Threads
International Workshop on Foundations of Object-Oriented Languages (FOOL 2008) January 2008 (FOOL 2008) : A. Lochbihler
2007
-
Jinja With Threads
Archive of Formal Proofs December 2007 : A. Lochbihler -
On Temporal Path Conditions in Dependence Graphs
7th IEEE Working Conference on Source Code Analysis and Manipulation (SCAM 2007) September 2007, pp. 49--58 (SCAM 2007) : A. Lochbihler, G. Snelting
2006
-
Temporal Path Conditions in Dependence Graphs
May 2006 : A. Lochbihler
Vorträge & Poster
- Quis custodiet ipsos custodes : The Java memory model. RS3 Jahrestreffen, Oktober 2012, München.
- Java and the Java Memory Model - a Unified, Machine-Checked Formalisation. ESOP, März 2012, Tallinn, Estland.
- Animating the Formalised Semantics of a Java-Like Language. GI FG Deduktion Jahrestreffen, Oktober 2012, Karlsruhe
- Quis custodiet ipsos custodes? RS3 Jahrestreffen, September 2011, Karlsruhe.
- Animating the Formalised Semantics of a Java-Like Language. ITP, August 2011, Nijmegen, Niederlande.
- A unified machine-checked model for multithreaded Java. Multi-Core Memory Models and Concurrency Theory, Januar 2011, Schloss Dagstuhl.
- Verifying a Compiler for Java Threads. ESOP, März 2010, Paphos, Zypern.
- Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs, August 2009, München.
- KESS - Die Komplexität evolutionär stabiler Strategien. Institut für Statistik und Decision Support Systems, Universität Wien, November 2008.
- Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLs, August 2008, Montreal, Kanada.
- Type Safe Nondeterminism - A Formal Semantics of Java Threads. FOOL, Januar 2008, San Francisco, CA.
- On Temporal Path Conditions in Dependence Graphs. SCAM, September 2007, Paris, Frankreich.
Gutachtertätigkeiten
- Zeitschriften: Computer Languages, Systems & Structures; Fundamenta Informaticae; Journal of Automated Reasoning
- Konferenzen: FSTTCS 2011, ESOP 2012, EMSOFT 2012
Lehre
- Vorlesung: Fortgeschrittene Objektorientierung , Sommersemester 2012
- Vorlesung: Semantik von Programmiersprachen , Sommersemester 2012
- Übung: Übungen zu Semantik von Programmiersprachen , Sommersemester 2012
- Vorlesung: Fortgeschrittene Objektorientierung , Sommersemester 2011
- Übung: Fortgeschrittene Objektorientierung , Sommersemester 2011, Beste Übung
- Vorlesung: Programmierparadigmen , Wintersemester 2010/2011
- Übung: Programmierparadigmen - Übungen , Wintersemester 2010/2011
- Vorlesung: Semantik von Programmiersprachen , Sommersemester 2010
- Übung: Übungen zu Semantik von Programmiersprachen , Sommersemester 2010
- Übung: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2009
- Vorlesung: Programmieren , Wintersemester 2008/2009
- Tutorium: Tutorien zu Programmieren , Wintersemester 2008/2009
- Übung: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2008
Projekte
Betreute Studien- und Abschlussarbeiten
abgeschlossen
- Verifizierte Implementierung von Patricia-Bäumen, Studienarbeit
- Funktionale Summary-Kanten-Berechnung für PDGs , Bachelor-/Studienarbeit
- Funktionale Konstruktion von Kontrollflussgraphen, Bachelor-/Studienarbeit
- Verifikation von Shivers funktionaler CFA-Analyse, Studienarbeit
- Übersetzer von Java nach Jinja, Studienarbeit