Research topics around program verification and security of applications
and platforms for trusted personal devices
Verification of concurrent Java programs, together with
Christian Haack and my former PhD
student Clement
Hurlin (now post doc at INRIA Bordeaux).
We have a particular interest in thread-modular
verification. This work is done in the context of the Mobius project.
Compositional specification and verification of programs with
procedures. This work is done in collaboration with Irem Aktug,Dilian Gurov
from KTH, Sweden and Christoph
Sprenger.
JML: use and
semantics. Particular interest in annotation generation to specify
security protocols. Currently, I am working on this with Alejandro
Tamalet. This work is done in the context of the Mobius project.