|title:||Extreme software reliability with Featherweight VerCors|
|keywords:||VerCors, Programming Languages, Concurrency|
|topics:||Logics and semantics|
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.