author: Bob Rubbens
title: Extreme software reliability with Featherweight VerCors
keywords: VerCors, Programming Languages, Concurrency
topics: Logics and semantics
committee: Sebastiaan Joosten
started: April 2019


Our tool, VerCors, allows programmer to verify the source code of their concurrent programs by adding annotations. VerCors verifies several constructions from Java, OpenMP, OpenCL, and programs in our own input language. This makes VerCors a large and impressive piece of software, and it increases the chance of bugs in VerCors. This project aims to solve that by developing or reusing a very small core language into which all or most of the features available in VerCors can be translated, and developing an independent highly trusted verifier for this core language along with a proof of concept through a trustable translation into this core language.