Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Making the Java memory model safe
Speaker:Andreas Lochbihler
coming from:ETH Zürich
Speakers Bio: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.
Event Type:Talk
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Tuesday, 14 July 2015
Duration:60 Minutes
Building:E1 5
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.
Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 07/03/2015 08:24 AM -- Created document.