author: Henk Mulder
title: Performance of software verification using Vercors
keywords: software verification, performance, tools
topics: Software Technology
committee: Luís Ferreira Pires ,
Sebastiaan Joosten ,
Marieke Huisman
started: January 2019

Description

The Vercors toolset can be used to verify memory safety and functional correctness of concurrent and parallel programs. By encoding the problem into an intermediate language the power of existing tools is leveraged to support additional concurrency models. However, for certain programs verification takes significant time.

In this research project you will formulate a plan to identify possible bottlenecks in verification by studying the techniques used to encode the problem to the intermediate language. You will think of: How can we identify possible bottlenecks in verification, how can we compare performance of different problem encodings and how can we integrate this in the project.