论文库

原文摘要

Formally verifying a method with Dafny guarantees correctness relative to its specification. However, a specification may be too permissive, allowing multiple outputs for the same input, even when the implementation produces only one. In this paper, we propose checkable certificates that provide independently verifiable evidence of whether a specification is weak or strong. A certificate of weakness contains an alternative implementation that verifies against the original specification, together with a witness input on which the original and alternative implementations produce different results. A certificate of strength is produced by constructing a harness around the original method such that successfully verifying the harness guarantees that the specification allows at most one possible output for any given input. We present DafnyCert, a tool that automatically produces these certificates. Strength is established by constructing and verifying the harness. Weakness is demonstrated by using the MutDafny mutation tool to find mutants that verify against the original specification, and by using the Hypothesis property-based testing framework to generate inputs that produce different outputs for the original program and the mutant. The resulting mutant and witness form a recheckable certificate of weakness. On a dataset of 3,910 verified Dafny methods from Dafny-Synthesis and VeriEquivBench, DafnyCert automatically certifies 3,570 methods (91.3%). We also provide certificates for the remaining 340 methods. To our knowledge, this is the first dataset in which every specification is backed by a checkable certificate of strength or weakness. These labels disagree with the benchmarks' original labels for 16.3% of the methods. These findings highlight the importance of supporting specification strength labels with independently checkable evidence.