Lehrstuhl Programmierparadigmen Logo Dipl.-Inf. Univ. Andreas Lochbihler
photo
Contact
Phone: +49 721 608-8352
E-Mail:
Address
IPD Prof. Snelting
Room 023
Adenauerring 20a
76131 Karlsruhe
Consultation Hours
Do 9-10 Uhr

Research interests

Formal semantics
I am currently working on a formal semantics for a large subset of Java including threads for both source and byte code. The semantics is based on the Jinja semantics by T. Nipkow und G. Klein and is formalised in the theorem prover Isabelle/HOL. For both the source code and byte code sematnics type safety is to be shown. Moreover, part of it is also a compiler to be formalized and verified that translates source code programs to observationally equivalent byte code programs.
The formalisation in progress is available for download in the Archive of Formal Proofs with project title Jinja with Threads.

Temporal path conditions
I also work on temporal path conditions for paths in program and system dependence graphs. They improve on boolean path conditions, which are used to make slicing more precise: By allowing to express temporal relationsships, they are more precise. By connecting them to a model checker, they are used to automatically generate "witness" traces for information flow along a specific path.

Publications

2010
A. Lochbihler : Verifying a Compiler for Java Threads. ESOP 2010
2009
A. Lochbihler : Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009
A. Lochbihler, G. Snelting : On Temporal Path Conditions in Dependence Graphs. JASE
2008
D. Wasserrab, A. Lochbihler : Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLS 2008
K. Etessami, A. Lochbihler : The Computational Complexity of Evolutionarily Stable Strategies. IJGT 2008
A. Lochbihler : Type Safe Nondeterminism - A Formal Semantics of Java Threads. FOOL 2008
2007
A. Lochbihler : Jinja With Threads. AFP 2007
A. Lochbihler, G. Snelting : On Temporal Path Conditions in Dependence Graphs. SCAM 2007
2006
A. Lochbihler : Temporal Path Conditions in Dependence Graphs.

Talks

  • 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.

Courses

Projects

Advised thesis subjects