@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.}
}

{"_id":"rp8FEWG4yGZGtbStg","bibbaseid":"mulder-performanceofprogramverificationwithvercors-2019","authorIDs":[],"author_short":["Mulder, H."],"bibdata":{"bibtype":"mastersthesis","type":"mastersthesis","month":"July","title":"Performance of program verification with VerCors","author":[{"firstnames":["Henk"],"propositions":[],"lastnames":["Mulder"],"suffixes":[]}],"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.","bibtex":"@MastersThesis{essay78496,\nmonth = {July},\ntitle = {Performance of program verification with VerCors},\nauthor = {Henk {Mulder}},\nyear = {2019},\nurl = {http://essay.utwente.nl/78496/},\nabstract = {Program verification is only as useful as its ability to produce results in a timely\nmanner. In this research we investigate what performance bottlenecks are in\nthe VerCors verification tool for concurrent programs. The aim is to identify\nthe cause of a performance bottleneck, in order to optimize the tool.\nWe introduce a technique to identify what properties of a program are more\ndifficult to verify. Using those results, we present solutions to two performance\nbottlenecks that were identified: 1. An alternative encoding of arrays is implemented\nin the tool which allows the tool to reason up to 4 times faster about\nprograms that make use of arrays. 2. Our research in generating triggers for\nquantified expressions show that speedups up to 30% are possible. Though further\nresearch is required to investigate if this solution can be generalized and\noptimized further.}\n}\n\n","author_short":["Mulder, H."],"key":"essay78496","id":"essay78496","bibbaseid":"mulder-performanceofprogramverificationwithvercors-2019","role":"author","urls":{"Paper":"http://essay.utwente.nl/78496/"},"metadata":{"authorlinks":{}},"downloads":1,"html":""},"bibtype":"mastersthesis","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","creationDate":"2019-08-05T16:23:13.576Z","downloads":1,"keywords":[],"search_terms":["performance","program","verification","vercors","mulder"],"title":"Performance of program verification with VerCors","year":2019,"dataSources":["2tJugFYAignELAmZo","zT4KxAXTKvhK2Hrr4","cCvCnPTRQYq3qPe9y"]}