Monday March 9, Jonathan Heinen successfully defended his PhD dissertation, entitled “Verification of Java Programs: A Graph Grammar Approach” for a jury consisting of Arend Rensink (Twente, NL), Thomas Seidl, Martin Grohe, and Joost-Pieter Katoen (all Aachen).  Jonathan’s dissertation deals with the automated verification of pointer operations in Java Bytecode programs using quantified LTL where graph properties are expressed as MSP formulas.