Automatic Precondition Generation For VerCors

Program verification is a field of computer science, which focuses on determining if a program functions correctly. This is done by defining pre- and postconditions and possibly other related specifications. However, the writing of these specifications is still very much a human task. One of the tools that suffers from this burden is the verification tool VerCors. To reduce this burden, algorithms have been proposed for generating preconditions based on postconditions. In this paper, we look at multiple currently available tools that use such algorithms to generate preconditions. We compare their use cases with the scenarios in which VerCors is usually used, looking at their overlap. We look further at a specific tool that shows higher potential, PGen, and see the value of integrating it within VerCors. This is done by testing on multiple self-made examples and a set of real-world examples, that are used to test VerCors. Using the results we determine if this tool should be implemented within VerCors.