University of Twente Student Theses
Automatic Precondition Generation For VerCors
Mol Lous, J. (2024) Automatic Precondition Generation For VerCors.
|
PDF
449kB |
| Abstract: | 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. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/100726 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page