Lecturing in the computer science department of the University of Twente, teaching
(concurrent) programming, the use of formal methods, and program
verification.
Programme mentor for Master specialisations
MTV and
ST and the graduate school program
DeSC.
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,
parallel and distributed applications
and platforms for trusted personal devices
Reliability of Concurrent and Distributed
Software. This work is done in the context of the NWO VICI
project Mercedes.
Verification of distributed software, together with Wytse
Oortwijn. This work is done in the context of the NWO TOP
project VerDi.
Monitoring of concurrent software. This work is done in the
context of the 3TU.NIRICT project 3TU.BSR.
Verification of concurrent data structures, together with
Afshin Amighi,
Stefan Blom,
Wojciech
Mostowski,
Marina
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
with
Saeed Darabi, and
Stefan Blom.
This work is done in the context of the CARP
project.
Within the project, we collaborate in particular with
Alastair Donaldson, and
Jeroen
Ketema from Imperial College, UK, and
Christina
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
and
Maurice
van Keulen.
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.
