Christian Haackchristian.h.haack at gmail
In February 2009, I have joined aicas realtime --- a company whose main product is a Java VM for embedded and real-time systems. Here I am spending most of my time contributing to the development and maintenance of the JamaicaVM and related tools. Moreover, I have been involved in the CHESS project --- a European applied research project on model-driven development for embedded systems.
From 2005 until January 2009, I worked as a researcher funded by the Mobius project, a European Integrated Project developing novel technologies for trustworthy global computing, focusing on the safety and security of Java applications for mobile phones and PDAs.
In January 2009, I taught a course at the COST Winter School on Verification of Object-Oriented Programs in Estonia.
In 2007 and 2008, I taught courses on Verification of Security Protocols, as part of a 2-year master track in computer security.
I have been working on verification techniques for multi-threaded Java programs, in particular on adapting concurrent separation logic to a Java-like setting. See my papers with Clement Hurlin and Marieke Huisman.
I have been working on pluggable type systems for specifying and checking object immutability in Java-like languages. I am particularly interested in type-based approaches that satisfactorily treat object initialization and encapsulated subobjects. See my papers with Erik Poll, Jan Schäfer and Aleksy Schubert. The extended annotation syntax JSR 308 and the associated checker framework provide a great basis for implementing such type systems.
I have been working on type systems for cryptographic protocols. These enforce prudent design practices that suffice to ensure certain security properties. See the Cryptyc typechecker and my papers with Alan Jeffrey.
I have been working on techniques for accurately locating sources of type errors in implicitly typed programming languages. See my papers with Joe Wells. At the time, I wrote a proof-of-concept type error slicer for a sublanguage of SML. Some of my examples are still used in the web demo of the current implementation for full SML.
I received a Ph.D. degree from Kansas State University. My dissertation was about semantics-based adaptation of software components. My supervisor was Alley Stoughton.
Last modified: Aug 12, 2012