About VSComp

What VSComp Is For

The Verified Software Competition was created to provide a practical testing ground for formal verification tools and techniques. The premise is straightforward: give participants a set of clearly specified programming tasks and ask them to prove, mechanically, that their implementations are correct. The resulting submissions reveal which tools handle which problem classes effectively, where specifications are difficult to write, and how the field is progressing from one year to the next.

This is not a contest in the conventional sense. There are no prizes in the traditional meaning of the word, and the emphasis is on the quality and completeness of the verification rather than speed. The competition serves the community by generating benchmarks, encouraging tool developers to address practical limitations, and giving researchers a shared set of problems to discuss and compare approaches against.

In practice, VSComp has functioned as a bridge between the theoretical foundations of program verification and the engineering reality of making proofs work on real code. The problems are grounded — sorting algorithms, data-structure invariants, concurrent protocols — and the solutions must be machine-checkable. This grounds the conversation in what verification tools can actually do, as opposed to what they might do in principle.

The People Behind the Competition

VSComp is sustained by a community of researchers, tool developers, and practitioners who share an interest in making formal verification more practical and more widely adopted. Organisers are listed on the year page when available. The organising committees for individual editions have drawn from universities and research institutions with strong programmes in formal methods, programming languages, and software engineering.

Participants come from a similarly broad base. Over the years, submissions have arrived from research groups at European, North American, Asian, and Australian institutions, as well as from industry practitioners who use verification tools in production settings. Graduate students have been well represented — the competition provides a valuable opportunity to test emerging skills against well-defined challenges.

The community also extends to those who use VSComp problems as teaching material or benchmarking suites. Several verification tools cite competition problems in their documentation or test suites, and instructors in formal-methods courses have used past problems as assignments. This secondary use was not the original intent, but it has become a meaningful part of the competition's impact.

The Verified Software Initiative

VSComp grew out of the Verified Software Initiative (VSI), a long-term international research effort aimed at developing the science, tools, and methodology needed to produce verified software at scale. The initiative, which brought together researchers from dozens of institutions, recognised that practical progress required not only theoretical advances but also concrete mechanisms for evaluating tools and techniques against shared benchmarks.

The competition was conceived as one such mechanism. By posing problems that are grounded in real programming tasks and requiring machine-checkable proofs, VSComp provides a repeatable, structured way to assess the state of the art. Each edition generates a snapshot of what verification tools can accomplish, and the series as a whole traces the field's trajectory over time.

The Verified Software Initiative also supported the VSTTE conference series, which provides a complementary forum for presenting research results. The connection between the competition and the conference is discussed in more detail below and on the history page.

Connection to VSTTE

VSTTE — Verified Software: Theories, Tools, Experiments — is a conference series dedicated to the science and engineering of verified software. VSComp has been closely associated with VSTTE since its inception. Several editions of the competition were co-located with VSTTE events, and competition reports have appeared in VSTTE proceedings.

The relationship is symbiotic. The conference provides a venue for discussing verification research at a theoretical and methodological level, while the competition provides concrete data about how those ideas perform in practice. Participants at VSTTE workshops have presented and discussed their competition solutions, and the resulting conversations have influenced both tool development and future problem design.

For details on which editions were associated with which conference events, consult the years index. The problems catalogue also notes the connection between specific challenges and the research themes of the corresponding VSTTE meeting.

How the Competition Is Run

Each edition of VSComp is organised by a small committee of researchers drawn from the formal-methods community. The committee is responsible for selecting problems, managing the submission process, evaluating solutions, and reporting results. Committee composition has varied between editions, reflecting the distributed nature of the community.

The competition operates entirely online. There is no physical venue for participation; problems are published electronically, and solutions are submitted through the competition infrastructure. This format was chosen to maximise accessibility — formal verification is a global field, and an online competition removes geographic barriers that would exclude many potential participants.

Organisers are listed on the year page when available. For general questions about the competition, the contact page provides guidance on how to reach the organising community.

Further Reading

If you are new to formal verification, the formal verification overview provides an introduction to the field, its techniques, and its relevance to software engineering. It is written for readers who may not have a background in formal methods but want to understand what the competition is about.

For the competition's chronological development, including how the format and problem selection evolved over time, see the history page. The years index provides direct access to edition-specific hub pages with detailed information about each year.