Dr. rer. nat. Andreas Lochbihler

	Contact Email: Bitte warten...

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, machine-checked 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: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

Talks

• Quis custodiet ipsos custodes : The Java memory model. RS3 annual meeting, October 2012, Munich.
• Java and the Java Memory Model - a Unified, Machine-Checked Formalisation. ESOP, March 2012, Tallinn, Estonia.
• Animating the Formalised Semantics of a Java-Like 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 Java-Like Language. ITP, August 2011, Nijmegen, Netherlands.
• A unified machine-checked model for multithreaded Java. Multi-Core 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 Object-Orientation , Sommersemester 2012
• Lecture: Semantics of programming languages , Sommersemester 2012
• Common Excercises: Tutorial for Semantics of programming languages , Sommersemester 2012
• Lecture: Advanced object-orientation , Sommersemester 2011
• Common Excercises: Advanced object-orientation , Sommersemester 2011, Beste Übung
• 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 object-orientation - exercises , Sommersemester 2009
• Lecture: Programming , Wintersemester 2008/2009
• Tutorial: Tutorial for Programming , Wintersemester 2008/2009
• Common Excercises: Übungen zu Fortgeschrittene Objektorientierung , Sommersemester 2008

Projects

• Quis-Custodiet
• VALSOFT/Joana

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