HOME | DEUTSCH | IMPRESSUM | KIT

Dr. rer. nat. Andreas Lochbihler

photo

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, 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

2013

2012

2011

2010

2009

2008

2007

2006

Talks

Reviewer

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

Courses

Projects

Advised thesis projects

finished