Since August 2015 I am a PhD candidate at the Formal Methods and Tools (FMT) research group at the University of Twente in Enschede, the Netherlands. My main research is focused on program logics, in particular separation logics, as well as program abstractions, process algebras, theorem proving, and high-performance, parallel and distributed (symbolic) model checking. I am currently working on verifying distributed software using both deductive and algorithmic reasoning. My Master's thesis, named Distributed Symbolic Reachability Analysis focuses more on high-performance model checking and can be found here.
I received my Master's degree with Honours, as result of attending the Master's Honours Research programme in addition to the regular Master's programme, named Methods and Tools for Verification (MTV). The topics of the MTV programme include: model checking, logic, static verification (model checking, deductive verification), dynamic (runtime) verification, and (model-based) testing.
DistBDD - a distributed symbolic reachability analysis implementation for high-performance networks of multi-core machines.
VerCors Verification Toolset - a toolset for verifying parallel and concurrent software (written in Java, C, OpenMP, or OpenCL).
Some documentation can be found here.
A detailed list of verified examples can be found here.
Try VerCors online here.
University of Twente,
Drienerlolaan 5, 7522 NB, Enschede.