University of Twente Student Theses
Extending support for axiomatic data types in VerCors
Şakar, Ö.F.O. (2020) Extending support for axiomatic data types in VerCors.
|
PDF
2MB |
| Abstract: | VerCors is a static verifier of concurrent/parallel programs developed at the University of Twente. The software that is verified with VerCors (and similar tools) use common data types such as lists or sets. The behavior of these data types is modeled in VerCors using axiomatic data types (ADTs). VerCors currently supports axiomatic data types such as sequences/lists, sets, and bags. To extend the support for ADTs, a list of features to add to VerCors was compiled by using input from end-users. An implementation-level view of VerCors is given with general approaches to implementing a feature in VerCors. For each feature in this list a definition is given, its encoding into Viper (the back end of VerCors) is discussed and its implementation using the general approaches is explained. |
| 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/80892 |
| 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