Extract, model, refine: improved modelling of program verification tools through data enrichment

(authored by agents unless marked 🧑) Tag: lathouwers2025extract, paper

purpose and contribution

This paper builds a megamodel and maintained data set for program-verification (PV) tools. Its scope includes “generative techniques, testing, model checking, theorem proving, etc.” (Section 1, p.1293). The result is ProVerB: tool pages, a PV-level taxonomy, tags, links, and API-enriched metadata. The abstract reports a “data set of 400+ program verification tools” and says practical fields such as last-commit dates are kept current through APIs (Abstract, p.1293).

technique 1: classify tools by PV0–PV6 proof roles

What it is: classify increasing correctness-control levels by what the user supplies and what the verifier/prover does. When to use it: use the levels to choose a tool or identify what evidence a claimed verification result actually provides.

Steps (Section 3, pp.1296–1298):

1. Identify the artefact and any claim about it.
2. Ask whether there is only an implicit formal model (PV0), a solver checking model well-formedness (PV1), or synthesis/repair filling holes (PV2).
3. For user-stated properties checked by an automated prover/verifier, classify PV3.
4. If properties are generated by a monoverifier, classify PV4.
5. If users define theories/specification languages compiled into checks, classify PV5.
6. If users construct proofs checked by a proof assistant, classify PV6.

The paper states: “PV0 tools give the least guarantees of correctness, whereas PV6 tools allow the user to work towards maximum correctness guarantees.” (Figure 1 caption, p.1296) Verus form (Inference): Verus is generally PV6 when users write contracts and proof functions checked by the verifier; an agent that only generates code/tests is PV2 or below. The taxonomy does not prove a tool sound; it organizes possible guarantees.

technique 2: reproducible tool-dataset harvesting

What it is: gather candidate tools from selected proceedings, create structured Markdown pages, and use light snowballing. When to use it: use this to build a searchable local map before comparing techniques or selecting a verifier.

Steps (Section 4.1, pp.1298–1301):

1. Select CAV 2017–2022 and TACAS 2016–2021 as tool-rich sources; this yielded 519 papers (406 CAV, 113 TACAS) (Section 4.1.1, p.1299).
2. Detect tool names from title patterns such as “Tool name: subtitle with explanation” (Section 4.1.2, p.1299).
3. Read each paper and tag the relation as Presents, Extends, Expands, or Uses (Section 4.1.2, p.1299).
4. Exclude entries without correctness guarantees, unnamed/unmaintained prototypes where no artefact exists, and non-PV libraries/formats (Sections 4.1.2–4.1.3, pp.1299–1300).
5. Create one Markdown page with name, domain, type, input/output, internals, relations, links, update dates, and inclusion reason (Section 4.1.3, p.1300).
6. Add a tool when at least two existing entries refer to it (light snowballing, Section 4.1.3, p.1300).
7. Double-check classifications among authors and consult source papers for disputes (Section 4.1.5, p.1300).

Inference: for VL, harvest Verus/vstd tools and studies into one page per verifier, preserving paper, repository, language, contracts, trusted base, and evidence fields. The paper’s source selection is conference-biased, so a VL corpus must include Rust and systems venues.

technique 3: ontology-based data enrichment

What it is: preserve a human-readable template while mapping entries to an ontology whose classes connect tools, repositories, articles, concepts, PV levels, conferences, writers, and code contributors. When to use it: use ontology enrichment when links and metadata must remain queryable and updateable without rewriting hand-curated descriptions.

Steps (Section 4.2, pp.1301–1302):

1. Preserve the existing data structure and automate maintenance (Section 4.2, p.1301).
2. Separate enrichment into new entries, new information, and improved information (Section 4.2, p.1301).
3. Instantiate Repository and Article objects from stored links; query GitHub, Springer, and Crossref APIs for commits, titles, abstracts, authors, and contributors (Section 4.2.1, p.1301).
4. Represent concepts/tags and PV classification as ontology classes, retaining manual content (Tables 1–2, p.1302).
5. Resolve author–contributor same-as relationships and optionally run the process weekly through GitHub workflows that open a reviewable pull request (Sections 4.2.1–4.2.2, pp.1301–1302).

The paper says: “The structure of the data set should be preserved.” (Section 4.2, p.1301) Verus form (Inference): model each Verus verifier as a stable record with typed fields for crate, Rust version, backend, specification language, trust assumptions, and benchmark evidence; derive repository and paper metadata automatically but review identity matches before accepting them.

technique 4: automated extraction from proceedings

What it is: use PDF pattern matching to bootstrap names, links, and keywords, then let humans resolve ambiguous cases. When to use it: use it to lower the cost of adding new papers while retaining manual semantic validation.

Steps (Sections 4.1.2 and 4.2, pp.1299, 1301):

1. Parse proceedings PDFs for title-shaped tool names, resource links, and keywords.
2. Insert the extracted values into the Markdown template and use keywords as initial tags.
3. Manually inspect papers that do not match the heuristic and confirm whether a detected item is actually a PV tool.
4. Preserve hand-added descriptions while scripts add or refresh machine-derived fields.

Inference: this is useful for VL’s local database, but extraction must never turn a paper’s mention of Verus into evidence that the paper verifies Rust. The authors report partial automation only; no extraction precision/recall denominator is supplied.

technique 5: trend analysis and dataset quality checks

What it is: summarize category counts, enrichment coverage, and source composition to assess what the dataset can support. When to use it: use denominators alongside counts so a catalog does not imply unsupported completeness.

Evidence: ProVerB contained 427 tools, 26 specification formats, and 71 tags (Section 4.3, p.1302). Counts by level were PV0 16, PV1 98, PV2 84, PV3 74, PV4 101, PV5 13, PV6 13, plus 46 no-PV and 8 to-categorize (Section 4.3, p.1302). Of 519 selected papers, 351 (68%) had identifiable tools, 54 (10%) unnamed prototypes, and 114 (22%) no tool (Table 3, p.1303); the 78% implementation figure is 351+54 divided by 519. Light snowballing added 76 tools (Section 4.3, p.1303).

Enrichment covered 400 of 427 Markdown files; APIs succeeded for 256 of 269 repositories and 518 of 525 articles (Section 4.3.1, p.1303). The authors identified 1,419 code contributors and 1,188 authors; exact-name matching found 273 same-as relationships and 169 tools with at least one overlapping expert, while they expect more because only exact matches were counted (Section 4.3.1, p.1303).

what is trusted, what fails, and VL impact

Classification is expert interpretation: “All the PV-classifications that we performed, come from our personal interpretations” (Section 6.1, p.1307). Double checking reduces but does not eliminate misclassification. Conference selection, title heuristics, missing APIs, exact-name identity matching, and excluded unnamed prototypes bias coverage. The dataset is observational and does not establish tool effectiveness or causal adoption benefits.

Inference: this work is directly useful for VL as an inventory and gap detector, not as a correctness argument. It already supplies the catalog pattern—levels, structured pages, provenance, and refresh workflows—that VL should reuse instead of rebuilding. VL should add Rust/Verus-specific fields and mark whether each tool checks executable behavior, contracts, compiler output, or only models. A large database does not itself lower the product threat from agent-written verified Rust: the threat remains specification error and incomplete coverage, which the PV level alone cannot expose.

techniques for the catalog

• PV0–PV6 megamodel: classify tools by user input and proof/verifier role
• proceedings harvesting: detect and manually validate tools from selected papers
• structured Markdown records: store inputs, outputs, internals, links, and provenance
• ontology enrichment: connect tools to repositories, articles, concepts, and people
• API refresh workflows: update commits and metadata automatically with reviewable changes
• coverage accounting: report counts with source and enrichment denominators Checked 2026-10-15 against paper lathouwers2025extract: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15