pith. sign in

arxiv: 2604.06877 · v1 · submitted 2026-04-08 · 💻 cs.LO

Predicate Subtypes in VerCors

Tycho Dubbeling (University of Twente) , Marieke Huisman (University of Twente) , \"Omer \c{S}akar (University of Twente) This is my paper

Pith reviewed 2026-05-10 16:59 UTC · model grok-4.3

classification 💻 cs.LO
keywords predicate subtypesprogram verificationVerCorsrange constraintsoverflow checkingspecifications
0
0 comments X

The pith

VerCors automatically generates specifications from predicate subtype declarations to enforce range constraints on variables.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to add predicate subtypes to the VerCors program verifier. These subtypes allow declaring range constraints on variables, and the system turns them into appropriate specifications automatically. It also supports combining several subtypes for one variable and adds a strict mode where all subexpressions must respect the bounds, which helps with overflow checks. This is implemented as a prototype in VerCors.

Core claim

Predicate subtypes provide a mechanism to specify range constraints on variable declarations. The approach in VerCors automatically generates specifications from these declarations, supports easy combination of multiple subtypes for a single variable, and introduces a strict mode for overflow checking where every subexpression must stay within the declared subtype.

What carries the argument

Predicate subtype declarations that trigger automatic generation of verification specifications.

If this is right

  • Users can declare range constraints without writing full specifications manually.
  • Multiple subtypes can be combined for one variable declaration.
  • Strict mode enables checking for overflows by enforcing bounds on all subexpressions.
  • A prototype implementation is integrated into the VerCors verifier.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar automatic generation could reduce specification effort in other program verifiers.
  • This approach might simplify proving absence of integer overflows in programs with bounded variables.

Load-bearing premise

The automatically generated specifications are semantically correct and sufficient for the verifier to prove properties without introducing unsoundness.

What would settle it

A program where using a predicate subtype leads to an incorrect verification result or fails to catch an overflow in strict mode.

Figures

Figures reproduced from arXiv: 2604.06877 by Marieke Huisman (University of Twente), \"Omer \c{S}akar (University of Twente), Tycho Dubbeling (University of Twente).

Figure 1
Figure 1. Figure 1: Example VerCors PVL program and specification [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example with predicate subtypes With this encoding, it is possible to specify that a variable should satisfy multiple predicates: this simple gives rise to multiple pre- or post-conditions, or assertions. More advanced approaches for com￾bining predicate subtypes are discussed in Section 3.3. 3.2 Example To illustrate our approach, consider the example in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Encoding of predicate subtypes in standard specifications [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Toy example illustrating the use of multiple ways to combine subtypes [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

3 major / 0 minor

Summary. The paper describes an extension to the VerCors program verifier for predicate subtypes. It claims that predicate subtype declarations can be automatically translated into appropriate specifications, that multiple subtypes can be combined for a single variable declaration, and that a strict mode can be used for overflow checking by requiring every subexpression to remain within the declared subtype. A prototype implementation of these features is integrated into VerCors.

Significance. If the generated specifications are semantically correct and the strict mode operates without introducing unsoundness or requiring excessive manual intervention, the work would enhance the practical usability of VerCors for specifying and verifying range constraints on variables. The contribution is primarily an engineering extension rather than a new theoretical result, and the lack of any soundness argument, implementation details, or evaluation results reduces its assessed impact.

major comments (3)
  1. Abstract: the central claim that specifications are 'automatically generated' and 'appropriate' is not supported by any description of the translation rules, any soundness argument, or any example showing the generated assertions for a predicate subtype declaration.
  2. Abstract: the strict mode is presented as enabling overflow checking, yet no definition is given for how subexpressions are constrained, how the mode interacts with the underlying verifier, or why it avoids introducing false positives or unsoundness.
  3. Abstract: the claim that the prototype is 'integrated into the VerCors verifier' is stated without any indication of the integration points, changes to the front-end or back-end, or verification conditions that were successfully discharged.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We are grateful to the referee for their constructive feedback. We address each of the major comments point by point and have prepared revisions to the manuscript to incorporate additional explanations and examples as suggested.

read point-by-point responses

  1. Referee: [—] Abstract: the central claim that specifications are 'automatically generated' and 'appropriate' is not supported by any description of the translation rules, any soundness argument, or any example showing the generated assertions for a predicate subtype declaration.

    Authors: We agree that the abstract, being a summary, does not include these elements. The manuscript body outlines our approach to automatically generating specifications from predicate subtype declarations. To better support the claim, we will revise the paper by adding a concrete example of a predicate subtype declaration along with the generated specifications. We will also include a high-level overview of the translation rules used. As this work is an engineering contribution extending an existing sound verifier, we maintain that the generated specifications are appropriate as they faithfully translate the subtype predicates into equivalent assertions; a detailed soundness argument can be added if required. revision: yes

  2. Referee: [—] Abstract: the strict mode is presented as enabling overflow checking, yet no definition is given for how subexpressions are constrained, how the mode interacts with the underlying verifier, or why it avoids introducing false positives or unsoundness.

    Authors: We will expand the description of the strict mode in the revised manuscript. Specifically, we will define that in strict mode, every subexpression is required to satisfy the subtype predicate, which is enforced by generating additional verification conditions for each operation. This interacts with VerCors by leveraging its existing assertion checking mechanism. It avoids unsoundness because it only adds constraints (making verification stricter), and false positives are mitigated by the fact that the mode is optional and users can choose when to apply it for overflow checks. An illustrative example will be included. revision: yes

  3. Referee: [—] Abstract: the claim that the prototype is 'integrated into the VerCors verifier' is stated without any indication of the integration points, changes to the front-end or back-end, or verification conditions that were successfully discharged.

    Authors: To address this, we will add details on the implementation in the revised version. The integration involves extending the parser in the front-end to recognize predicate subtype syntax in variable declarations and modifying the specification generation component in the back-end to produce the corresponding assertions. We will also report on specific verification conditions, such as those for range-constrained integer operations, that were successfully discharged by the prototype. revision: yes

Circularity Check

0 steps flagged

No significant circularity in implementation description

full rationale

The paper describes a prototype implementation for adding predicate subtypes to the VerCors verifier. It explains automatic generation of specifications from subtype declarations, support for combining multiple subtypes on one variable, and a strict mode for overflow checking. No mathematical derivations, equations, fitted parameters, predictions, or self-referential claims appear in the provided text or abstract. The contribution is an engineering extension rather than a theoretical result with a derivation chain, so no steps reduce to inputs by construction. This is a self-contained description of an implementation.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is an implementation and prototype paper with no mathematical content; no free parameters, axioms, or invented entities are introduced.

pith-pipeline@v0.9.0 · 5389 in / 964 out tokens · 52410 ms · 2026-05-10T16:59:53.758307+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

  1. [1]

    Amighi, C

    A. Amighi, C. Haack, M. Huisman & C. Hurlin (2015): Permission-based separation logic for multithreaded Java programs. LMCS 11(1), doi:10.2168/LMCS-11(1:2)2015

    work page doi:10.2168/lmcs-11(1:2)2015 2015

  2. [2]

    In: Proc

    Lukas Armborst, Pieter Bos, Lars B. van den Haak, Marieke Huisman, Robert Rubbens, Ömer ¸ Sakar & Philip Tasche (2024): The VerCors Verifier: A Progress Report. In Arie Gurfinkel & Vijay Ganesh, editors: Computer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II, Lecture Notes in Co...

    work page doi:10.1007/978- 2024

  3. [3]

    In: Object-Oriented Programming Sys- tems, Languages, and Applications (OOPSLA), 147:1–147:30

    V . Astrauskas, P. Müller, F. Poli & A. J. Summers (2019): Leveraging Rust Types for Modular Specification and Verification. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) , 3, ACM, pp. 147:1–147:30, doi:10.1145/3360573. Available at https://www.youtube.com/watch?v= lfc08mntlB0

    work page doi:10.1145/3360573 2019

  4. [4]

    Available at https://frama-c.com/download/wp-manual-Chlorine-20180501.pdf

    Patrick Baudin, François Bobot, Loïc Correnson & Zaynah Dargaye: WP Plug-in Manual . Available at https://frama-c.com/download/wp-manual-Chlorine-20180501.pdf

    work page

  5. [5]

    Bornat, C

    R. Bornat, C. Calcagno, P.W. O’Hearn & M.J. Parkinson (2005): Permission accounting in separation logic. In: POPL, pp. 259–270, doi:10.1145/1040305.1040327

    work page doi:10.1145/1040305.1040327 2005

  6. [6]

    Boyland (2003): Checking Interference with Fractional Permissions

    J. Boyland (2003): Checking Interference with Fractional Permissions . In Radhia Cousot, editor: SAS, LNCS 2694, Springer, pp. 55–72, doi:10.1007/3-540-44898-5_4. Dubbeling, Huisman & ¸ Sakar 67

    work page doi:10.1007/3-540-44898-5_4 2003

  7. [7]

    Available at https://dafny.org/latest/DafnyRef/DafnyRef

    (2025): Dafny Reference Manual. Available at https://dafny.org/latest/DafnyRef/DafnyRef. Last visited: January 4, 2026

    work page 2025

  8. [8]

    Summers & Peter Müller (2025): Fifteen Years of Viper

    Marco Eilers, Malte Schwerhoff, Alexander J. Summers & Peter Müller (2025): Fifteen Years of Viper. In Ruzica Piskac & Zvonimir Rakamaric, editors:Computer Aided Verification - 37th International Conference, CA V 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part I, Lecture Notes in Computer Science15931, Springer, pp. 107–123, doi:10.1007/978-3-0...

    work page doi:10.1007/978-3-031-98668-0_5 2025

  9. [9]

    Available at https:// frama-c.com/download/rte-manual-Sulfur-20171101.pdf

    Philippe Herrmann & Julien Signoles: Frama-C’s annotation generator plug-in. Available at https:// frama-c.com/download/rte-manual-Sulfur-20171101.pdf

    work page

  10. [10]

    doi:10.1145/363235.363259

    C.A.R. Hoare (1969): An axiomatic basis for computer programming. Communications of the ACM 12(10), pp. 576–580, doi:10.1145/363235.363259

    work page doi:10.1145/363235.363259 1969

  11. [11]

    Springer, doi:10.1007/978-3-031-55608-1

    Nikolai Kosmatov, Virgile Prevosto & Julien Signoles, editors (2024): Guide to Software Verification with Frama-C. Springer, doi:10.1007/978-3-031-55608-1

    work page doi:10.1007/978-3-031-55608-1 2024

  12. [12]

    Available athttps://viperproject.github.io/prusti-dev/dev-guide/ encoding/types-heap.html

    Heap-based type encoding. Available athttps://viperproject.github.io/prusti-dev/dev-guide/ encoding/types-heap.html

    work page

  13. [13]

    Shankar (1998): Subtypes for Specifications: Predicate Subtyping in PVS

    John Rushby, Sam Owre & N. Shankar (1998): Subtypes for Specifications: Predicate Subtyping in PVS . IEEE Transactions on Software Engineering 24, pp. 709–720, doi:10.1109/32.713327. Available at https: //ieeexplore.ieee.org/abstract/document/713327

    work page doi:10.1109/32.713327 1998