Andreas Lochbihler is a senior researcher in David Basin's group at the ETH Zürich. His research focuses on deriving machine-checked implementations from protocol specifications such that the security properties of the model are preserved. Before joining the ETH, he was a member of Gregor Snelting's groups at the Karlsruhe Institute of Technology and the University of Passau. He received his PhD from the KIT in 2012. In his thesis, he 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.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

Type safety and the Java security architecture distinguish the Java programming language from other mainstream programming languages like C and C++. Another distinctive feature of Java is its built-in support for multithreading and the Java memory model. In this talk, I discuss how the current Java memory model affects type safety and Java's security guarantees.

The findings are based on a formal model of Java and the JMM. It includes dynamic memory allocation, thread spawns and joins, infinite executions, the wait-notify mechanism, and thread interruption, all of which interact in subtle ways with the memory model. The language is type safe and provides the data race freedom guarantee. The model and proofs have been checked mechanically in the proof assistant Isabelle.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only