University of Twente Student Theses
AValAnCHE: Improving robustness of the VerCors verification toolset using fuzzing
Nauta, Wander (2025) AValAnCHE: Improving robustness of the VerCors verification toolset using fuzzing.
|
PDF
1MB |
| Abstract: | VerCors is a verification toolset for sequential and concurrent programs. Given a suitably annotated program, written in one of a variety of programming languages, it can show both functional correctness and data race freedom. The applicability and usability of the toolset has already been shown in a number of case studies. However, VerCors cannot yet be used to verify its own correctness: it is written in Scala, which is not one of the supported programming languages. The toolset as a whole is also much larger and more complex than programs verified so far. Instead, automated tests are used to increase confidence in its correctness and robustness, and so confidence in its results. We have investigated whether adding fuzzing to the VerCors testing strategy could aid in finding robustness issues in VerCors itself, especially in the face of unexpected inputs. We have shown that grammar-based fuzzing can be successfully used to find robustness issues in VerCors. In total, we have found 28 confirmed new crashing bugs in the toolset. To support our comparison of different fuzzing approaches and aid integration into the VerCors testing strategy, we have developed a tool tailored to VerCors itself. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/106440 |
| 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