Benchmarks

What Are Verification Benchmarks?

A verification benchmark is a problem — typically a programming task with a formal specification — that is used to evaluate the effectiveness of a verification tool or technique. Good benchmarks are precisely specified so that there is no ambiguity about what constitutes a correct solution. They are grounded in realistic programming patterns so that the results are relevant to practical software development. And they cover a range of difficulty levels and problem domains so that different aspects of a tool's capabilities can be assessed.

Benchmarks matter because claims about verification tools are difficult to evaluate in the abstract. A tool developer might assert that their system handles pointer reasoning or concurrency effectively, but without concrete evidence — a set of problems solved, a comparison with other tools — such claims are hard to assess. Benchmarks provide that evidence. They turn qualitative claims into quantitative data: which problems can a tool solve, how much human effort is required, how long does the automated reasoning take, and how complete is the resulting proof?

How VSComp Problems Serve as Benchmarks

The problems published for each VSComp edition were designed primarily as competition challenges, but they have acquired a secondary life as benchmarks. This was not entirely unintentional — the competition organisers recognised from the outset that a well-specified, publicly available set of verification challenges would have value beyond the competition itself. In practice, VSComp problems have been adopted as benchmarks by tool developers, used in academic papers as case studies, and incorporated into university courses as teaching exercises.

Several properties make VSComp problems effective benchmarks. They span multiple problem domains: sorting algorithms, search procedures, data-structure invariants, arithmetic computations, and concurrent protocols. They vary in difficulty, from problems that can be handled by most modern tools to problems that challenge even the most capable systems. And they come with documented solutions from multiple tools, providing a basis for comparison.

The competition years pages provide access to the problems from each edition, along with information about how participants approached them. The solutions archive documents the tools and techniques used, making it possible to compare approaches across different verification systems.

Tools Used in VSComp

Over the course of its editions, VSComp has attracted submissions using a wide variety of verification tools. Each tool brings a different approach to the verification task — different specification languages, different proof strategies, different degrees of automation. Understanding these tools provides context for interpreting benchmark results.

How Benchmarks Help Evaluate Tool Progress

The value of a benchmark suite lies not just in individual problem-solving but in the ability to track progress over time and compare tools against one another. When the same problem is solved by multiple tools — as happens in VSComp — the resulting solutions can be compared along several dimensions: the degree of automation achieved, the amount of annotation required, the time spent on proof construction, the completeness of the verification, and the clarity of the proof artefacts.

This comparative perspective is one of the most useful outputs of the competition. A problem that required extensive manual proof guidance in 2010 might be handled almost automatically by improved tools in 2017. A specification pattern that caused difficulties for one tool might be straightforward for another. These observations help tool developers identify areas for improvement and help users choose the right tool for their verification needs.

The competition does not produce formal rankings or scores. Instead, the evaluation committee assesses each submission on three dimensions — correctness, completeness, and clarity — and provides qualitative feedback. This approach reflects the nature of verification work: a partial but rigorous proof may be more valuable than a complete but superficial one, and the quality of a solution depends on context in ways that a single numerical score cannot capture.

Comparison Methodology

Comparing verification tools is inherently difficult. Different tools target different languages, use different specification formalisms, and make different trade-offs between automation and expressiveness. A fair comparison requires careful attention to what is being measured and an honest acknowledgement of what the comparison does not capture.

VSComp addresses this by defining problems in language-independent terms. The specification describes what the program should do, not how it should be implemented. This allows participants to choose whatever language and tool they prefer, and the evaluation focuses on the quality of the verification rather than the choice of tool. The result is not a tool ranking but a landscape — a picture of how different approaches perform on different classes of problems.

Researchers who use VSComp problems as benchmarks in their own work should be aware of this context. A tool that solves a particular VSComp problem is demonstrating capability on that problem, not claiming superiority over tools that took a different approach or chose different problems to focus on. The formal verification overview provides background on the different techniques that these tools employ.