Research: program verification and security of concurrent and
parallel applications
and platforms for trusted personal devices
Verification of concurrent data structures, together with
Afshin Amighi,
Stefan Blom,
Wojciech Mostowski,
Marina Zaharieva-Stojanovski, and my former PhD
student
Clement
Hurlin (now at Prove & Run, France). We use a variant of
permission-based separation logic to reason about
multithreaded programs. This work is done in the context of the VerCors project. This worked was started in th context of the Mobius project, when also
Christian Haack was
involved in this work.
Verification of GPGPU programs. We study in particular how permission-based separation
logic can be used to reason about OpenCL kernels. This work is done in the context of the CARP
project.
Security by Logic: Model Checking of Security Properties for
Multithreaded Programs. We study the specification and
verification of confidentiality, integrity and
availability for multithreaded programs. This work is done
in collaboration with Ngo Minh
Tri in the context of the SlaLoM project.
Persistent Functional Databases: how to use a persistent functional
programming language to develop a database management system
with natural support for parallellism, fine-grained locking
and optimal performance. This work is done in collaboration
with Lesley Wevers.
JML: use and
semantics. Particular interest in use of JML in education, and annotation generation to specify
security protocols. I have been working on this with Alejandro
Tamalet.
