Winner of the Netherlands
Prize for ICT Research 2013, worth 50,000 euros. The ICT Prize is a unique prize for a scientist, aged 40 years or younger, who carries out innovative research or is responsible for a scientific breakthrough in ICT.
Research: program verification and security of concurrent and
and platforms for trusted personal devices
Verification of concurrent data structures, together with
Zaharieva-Stojanovski. We use a variant of
permission-based separation logic to reason about
multithreaded programs. This work is done in the context
of the ERC Starting Grant VerCors project. This worked was started in th context of the Mobius project, when also
Clément Hurlin and Christian Haack were
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, together
Saeed Darabi, and
This work is done in the context of the CARP
Within the project, we collaborate in particular with
Alastair Donaldson, and
Ketema from Imperial College, UK, and
Jansen from RWTH Aachen, Germany.
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