Contact Email: >>please click this text<< 

In December 2012, I have left the KIT. I am now a postdoc at the ETH Zurich in David Basin's group. Please go to my new homepage
Research interests
Formal semantics
As part of my PhD thesis, I worked on a formal, machinechecked model of Java including threads for both source code and bytecode.
The model, which is formalised in the proof assistant Isabelle/HOL, extends the Jinja language by T. Nipkow and G. Klein and covers now all language and synchronisation primitives for threads and the Java memory model.
The semantics for source code and bytecode are executable and proven to be type safe.
The model also incldues a formalised, verified and executable compiler that translates source code programs into bytecode and preserves types and semantics.
The formalisation has been published in the Archive of Formal Proofs under the title Jinja with Threads, where it can also be downloaded.
I have also developed the conversion tool Java2Jinja as an Eclipse plugin to convert Java programs to JinjaThreads' input syntax.
Theorem proving
Code extractors permit to automatically translate formal models into executable prototypes.
In this area, I am mainly interested in how to extract efficient prototypes from formal specifications in the proof assistant Isabelle/HOL.
Among others, I focus on how to simplify using efficient data structures in the prototype without cluttering the specification.
Program analysis
The static program analysis slicing determines how different parts of a program might influence each other.
This can be used to control in information flow in programs and systems.
To improve the precision of discovery of and information about such influences, I developed in my master's thesis temporal path conditions.
By connecting them to a model checker, they are used to automatically generate "witness" traces for information flow along a specific path.
In this context, I am also interested in ensuring that the analyses themselves are sound. To that end, I work on executable prototypes for verified formalisations of such algorithms.
Publications
2014

Making the Java Memory Model Safe
ACM Transactions on Programming Languages and Systems 2014, pp. 12:112:65 : A. Lochbihler
2013

Lightweight 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 
Lightweight containers for Isabelle: efficient, extensible, nestable
Interactive Theorem Proving 2013, pp. 116132 (ITP 2013) : A. Lochbihler
2012

The Java Memory Model is Type Safe
December 2012 : A. Lochbihler 
A MachineChecked, TypeSafe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
July 2012 : A. Lochbihler 
Java and the Java Memory Model  a Unified, MachineChecked Formalisation
Programming Languages and Systems March 2012, pp. 497517 (ESOP 2012) : A. Lochbihler
2011

A Unified, MachineChecked Formalisation of Java and the Java Memory Model
December 2011 : A. Lochbihler 
Animating the Formalised Semantics of a Javalike Language
Interactive Theorem Proving 2011, pp. 216232 (ITP 2011) : A. Lochbihler, L. Bulwahn
2010

The Isabelle Collections Framework
July 2010, pp. 339354 (ITP 2010) : P. Lammich, A. Lochbihler 
Gateway Decompositions for Constrained Reachability Problems
Proceedings of the 9th International Symposium on Experimental Algorithms May 2010, pp. 449461 (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. 427447 (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. 310326 (TPHOLs 2009) : A. Lochbihler 
On Temporal Path Conditions in Dependence Graphs
Journal of Automated Software Engineering June 2009, pp. 263290 (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. 294309 (TPHOLS 2008) : D. Wasserrab, A. Lochbihler 
The Computational Complexity of Evolutionarily Stable Strategies
International Journal of Game Theory April 2008, pp. 93113 : K. Etessami, A. Lochbihler 
Type Safe Nondeterminism  A Formal Semantics of Java Threads
International Workshop on Foundations of ObjectOriented 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. 4958 (SCAM 2007) : A. Lochbihler, G. Snelting
2006

Temporal Path Conditions in Dependence Graphs
May 2006 : A. Lochbihler
Talks
 Quis custodiet ipsos custodes : The Java memory model. RS3 annual meeting, October 2012, Munich.
 Java and the Java Memory Model  a Unified, MachineChecked Formalisation. ESOP, March 2012, Tallinn, Estonia.
 Animating the Formalised Semantics of a JavaLike Language. GI FG Deduction annual meeting, October 2012, Karlsruhe
 Quis custodiet ipsos custodes? RS3 annual meeting, September 2011, Karlsruhe.
 Animating the Formalised Semantics of a JavaLike Language. ITP, August 2011, Nijmegen, Netherlands.
 A unified machinechecked model for multithreaded Java. MultiCore Memory Models and Concurrency Theory, January 2011, Schloss Dagstuhl.
 Verifying a Compiler for Java Threads. ESOP, March 2010, Paphos, Cyprus.
 Formalising FinFuns  Generating Code for Functions as Data from Isabelle/HOL. TPHOLs, August 2009, Munich, Germany.
 KESS  Die Komplexität evolutionär stabiler Strategien. Institute for Statistics and Decision Support Systems, University of Vienna, November 2008.
 Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLs, August 2008, Montreal, Canada.
 Type Safe Nondeterminism  A Formal Semantics of Java Threads. FOOL, January 2008, San Francisco, CA.
 On Temporal Path Conditions in Dependence Graphs. SCAM, September 2007, Paris, France.
Reviewer
 Journals: Computer Languages, Systems & Structures; Fundamenta Informaticae; Journal of Automated Reasoning
 Conferences: FSTTCS 2011, ESOP 2012, EMSOFT 2012
Courses
 Lecture: Advanced ObjectOrientation , Sommersemester 2012
 Lecture: Semantics of programming languages , Sommersemester 2012
 Common Excercises: Tutorial for Semantics of programming languages , Sommersemester 2012
 Lecture: Advanced objectorientation , Sommersemester 2011
 Common Excercises: Advanced objectorientation , Sommersemester 2011
 Lecture: Programming Paradigms , Wintersemester 2010/2011
 Common Excercises: Programming Paradigms  Exercises , Wintersemester 2010/2011
 Lecture: Semantics of programming languages , Sommersemester 2010
 Common Excercises: Tutorial for Semantics of programming languages , Sommersemester 2010
 Common Excercises: Advanced objectorientation  exercises , Sommersemester 2009
 Lecture: Programming , Wintersemester 2008/2009
 Tutorial: Tutorial for Programming , Wintersemester 2008/2009
 Common Excercises: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2008
Projects
Advised thesis projects
finished
 Verified Implementation of Patricia trees, study thesis
 Functional summary edge computation for PDGs, bachelor/study thesis
 Constructing control flow graphs in a functional language, bachelor/study thesis
 Verifiying Shiver's functional CFA analysis, study thesis
 Compiler from Java to Jinja, study thesis