Performance of program verification with VerCors. Mulder, H. Master's thesis, July, 2019.
Performance of program verification with VerCors [link]Paper  abstract   bibtex   2 downloads  
Program verification is only as useful as its ability to produce results in a timely manner. In this research we investigate what performance bottlenecks are in the VerCors verification tool for concurrent programs. The aim is to identify the cause of a performance bottleneck, in order to optimize the tool. We introduce a technique to identify what properties of a program are more difficult to verify. Using those results, we present solutions to two performance bottlenecks that were identified: 1. An alternative encoding of arrays is implemented in the tool which allows the tool to reason up to 4 times faster about programs that make use of arrays. 2. Our research in generating triggers for quantified expressions show that speedups up to 30% are possible. Though further research is required to investigate if this solution can be generalized and optimized further.
@MastersThesis{essay78496,
month = {July},
title = {Performance of program verification with VerCors},
author = {Henk {Mulder}},
year = {2019},
url = {http://essay.utwente.nl/78496/},
abstract = {Program verification is only as useful as its ability to produce results in a timely
manner. In this research we investigate what performance bottlenecks are in
the VerCors verification tool for concurrent programs. The aim is to identify
the cause of a performance bottleneck, in order to optimize the tool.
We introduce a technique to identify what properties of a program are more
difficult to verify. Using those results, we present solutions to two performance
bottlenecks that were identified: 1. An alternative encoding of arrays is implemented
in the tool which allows the tool to reason up to 4 times faster about
programs that make use of arrays. 2. Our research in generating triggers for
quantified expressions show that speedups up to 30% are possible. Though further
research is required to investigate if this solution can be generalized and
optimized further.}
}

Downloads: 2