University of Twente Student Theses

Login

Extending support for axiomatic data types in VerCors

Şakar, Ö.F.O. (2020) Extending support for axiomatic data types in VerCors.

[img] 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:http://purl.utwente.nl/essays/80892
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page