Verifier acceptance can miss weak generated contracts
Questa pagina non ha ancora una traduzione verificata. È mostrata la versione inglese. Leggi la versione inglese
In parole semplici
A program verifier checks whether a program keeps the promises written in its contract. But a contract can leave out an important promise or make a promise that says almost nothing, and the program may still pass.
VerusEval is a framework that checks generated contracts in several ways, including test cases and comparisons with reference contracts. In the study, fewer than half of the accepted artifacts cleared all three semantic checks without a flag. Passing the verifier alone did not show that a contract was correct.
La ricerca
When a verifier accepts a generated contract, does that mean the contract captures the program’s intended behavior? Acceptance checks only whether the implementation satisfies the supplied contract.
A missing guarantee, excluded valid input, or vacuous condition can still pass, leaving contract quality uncertain.
VerusEval combines proof checks, reference comparisons and input–output cases to assess generated contracts beyond whether Verus accepts them.
The study applied VerusEval to generated contracts from 18 configurations across 762 tasks. Among 7,081 artifacts accepted by Verus, researchers checked for vacuity, behavior on available input–output cases, and agreement with reference contracts. Only 42.3% cleared all three checks without a flag.
This supports the conclusion that acceptance alone is an incomplete quality signal: it establishes that the implementation satisfies its supplied contract, not that the contract describes intended behavior.
The checks add evidence, but a flag can be inconclusive and passing them does not prove correctness.
These checks depend partly on reference contracts and finite test cases, so passing them does not prove correctness. The study used one generation per task, one Verus release, and self-contained tasks that may not represent repository-scale verification.
Analisi
Dettagli
- Autori del paper originale
- Ding Wang, Chao Jiang, Dugang Liu, Zhiwu Xu, Cheng Wen
- Inviato ad arXiv
- Licenza
- arXiv non-exclusive