Description

This paper looks at an axiomatic data type, namely sequences, of the VerCors tool set and asks the following questions:

- [Research Question 1] What features are currently not supported by VerCors, but are supported by other software verification tools?
- [Research Question 2] How can these features, or a subset thereof with only features deemed important by the users of VerCors, be implemented without altering the current functionality of VerCors?

It finds that VerCors does not provide as many features for its sequences as Viper and Dafny, and that some of these features are missed by its users.
This paper shows an approach to add some of those missing features to VerCors, specifically to its sequences, and to verify these features work and do not alter the current functionality of VerCors.
This approach can be used to add more features to VerCors and verify them, also outside of sequences.