Predicate Subtypes in VerCors
This work addresses the need for more precise and automated verification of program constraints, particularly for developers using the VerCors verifier, but it is incremental as it builds on existing verification tools.
The paper tackles the problem of specifying range constraints on variable declarations by adding support for predicate subtypes to the VerCors program verifier, resulting in a prototype implementation that automatically generates specifications and includes a strict mode for overflow checking.
Predicate subtypes provide an attractive mechanism to specify range constraints on variable declarations. This paper discusses how we add support for predicate subtypes to the VerCors program verifier. Our approach automatically generates appropriate specifications from predicate subtype declarations. It provides support to easily combine multiple subtypes for a single variable declaration. Moreover, in order to use predicate subtypes for overflow checking, a special strict mode is introduced, where every subexpression also has to stay within the declared subtype. A prototype implementation is integrated into the VerCors verifier.