Lochbihler, Andreas, Dr.

Dr.  Andreas Lochbihler


ETH Zürich

Dep. of Computer Science 

Dr. Andreas Lochbihler

Institut f. Informationssicherheit 

CNB  F 109.2 

Universitätstrasse 6

8092 Zürich


  • phone +41 44 632 84 70 
  • mail
  • vcard www.infsec.ethz.ch/people/andreloc
  • vcard V-Card (vcf, 1kb)

About me

I am a senior researcher in David Basin's group at the ETH Zürich working in the project FCSPI. My research focuses on deriving machine-checked implementations from protocol specifications such that the security properties of the model are preserved. Before joining the ETH, I was a member of Gregor Snelting's groups at the Karlsruhe Institute of Technology and the University of Passau. I received my PhD from the KIT in 2012. In my thesis, I built a formal model of Java concurrency which formalises source code, bytecode, a virtual machine, the compiler and the Java memory model in the proof assistant Isabelle/HOL.


Lectures and exercise classes


If you are looking for a student project or thesis in the area of functional programming, mechanised theorem proving, or theory of programming languages, please contact me. Currently, I propose the following, but I am always open to your own ideas, too.

Theses proposals

B = Bachelor's thesis, M = Master's thesis,
M/B = Master's thesis that can be cut down to a Bachelor's
B/M = Bachelor's thesis that can be extended to a Master's

Supervised theses

I am supervising or have (co-)supervised the following theses.








  • Andreas Lochbihler: The Java Memory Model is Type Safe. Karlsruhe Reports in Informatics, Technical Report, No. 2012-23, December 2012.
    Link - BibTeX (BIB, 284 Bytes)
  • Andreas Lochbihler: A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler. PhD thesis, Karlsruher Institut für Technologie, Fakultät für Informatik, July 2012.
    Link - BibTeX (BIB, 419 Bytes)
  • Andreas Lochbihler: Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation. In: Helmut Seidl (Ed.), Programming Languages and Systems (ESOP 2012), LNCS 7211, pp. 497--517, Springer, March 2012.
    Original article available at springerlink.com - Preprint PDF (PDF, 468 KB) - BibTeX (BIB, 478 Bytes) - slides (PDF, 633 KB)


  • Andreas Lochbihler and Lukas Bulwahn: Animating the Formalised Semantics of a Java-like Language. In: Marko van Eekelen and Herman Geuvers and Julien Schmalz and Freek Wiedijk (Eds.), Interactive Theorem Proving (ITP 2011), LNCS 6898, pp. 216--232, Springer, 2011.
    Original article available at springerlink.com - Preprint PDF (PDF, 243 KB) - BibTeX (BIB, 518 Bytes) - slides (PDF, 300 KB)
  • Andreas Lochbihler: A Unified, Machine-Checked Formalisation of Java and the Java Memory Model. Karlsruhe Reports in Informatics, Technical Report, No. 2011-34, December 2011.
    Link - BibTeX (BIB, 324 Bytes)






Posters and further talks


  • Java2Jinja, an Eclipse plugin, converts Java programs to JinjaThreads syntax and provides a front-end to the JinjaThreads compiler, interpreter, and VM.
Page URL: http://www.infsec.ethz.ch/people/detail.html
© 2017 Eidgenössische Technische Hochschule Zürich