Predicate Subtypes in VerCors
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908947477168128 |
|---|---|
| author | Dubbeling, Tycho Huisman, Marieke Şakar, Ömer |
| author_facet | Dubbeling, Tycho Huisman, Marieke Şakar, Ömer |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_06877 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Predicate Subtypes in VerCors Dubbeling, Tycho Huisman, Marieke Şakar, Ömer Logic in Computer Science 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. |
| title | Predicate Subtypes in VerCors |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2604.06877 |