Publications

Why Competitions Produce Publications

Formal verification competitions serve a dual purpose. They are a practical exercise — participants test their tools and skills against concrete challenges — but they also generate data about the state of the art. Which tools handle which problem classes well? Where do specifications become ambiguous? How do different proof strategies compare when applied to the same task? These are questions that interest the research community, and competition reports are a natural vehicle for exploring them.

Not every edition has produced a formal publication. In some years, results were communicated primarily through the competition infrastructure and the associated workshop sessions. In others, detailed reports appeared in conference proceedings or as standalone technical notes. The records below reflect what has been published; where a formal publication is not available for a given year, the relevant year page provides whatever documentation exists.

Many of these publications are indexed in academic databases. The ACM Digital Library is one such resource where proceedings from formal-methods venues, including those associated with VSComp, can be found. Researchers looking for citation metadata or full-text access through institutional subscriptions may find it a useful starting point.

Documented Editions

The following entries summarise the publications associated with each documented edition of VSComp. Each entry includes the year, the title of the report, the venue where it appeared, and a brief description of its content and scope.

2010 — The 1st Verified Software Competition: Experience Report

Venue: VSTTE 2010 Workshop / Lecture Notes in Computer Science

The report from the inaugural edition documents the competition format, the five problems set, and a summary of the approaches taken by participants. It discusses the design rationale for the problem selection and offers observations on the state of verification tools as assessed through competition entries. Published as part of the VSTTE 2010 post-proceedings.

2011 — VSComp 2011: Competition Problems and Solutions Overview

Venue: VSTTE 2012 Workshop Proceedings

This report covers the second edition, including the refined problem set and the evolution of the submission format from the pilot year. It contains a structured comparison of solution approaches, noting which tools participants selected for each problem and how completeness varied across entries. The report appeared in the post-proceedings of the associated VSTTE workshop.

2012 — Verified Software Competition 2012: Problem Descriptions and Results

Venue: Technical Report / Workshop Notes

The third edition introduced problems that placed greater emphasis on data-structure invariants and concurrency. This report presents the problem specifications, summarises the solutions received, and discusses the evaluation process. It reflects the growing maturity of both the competition format and the participating tool ecosystems.

2014 — The 2014 Verified Software Competition

Venue: STTT (Software Tools for Technology Transfer) / LNCS

A more substantial publication than the earlier reports, this paper provides detailed problem descriptions, a taxonomy of the verification approaches used, and a comparative analysis of solution quality. It includes discussion of specification ambiguity — cases where participants interpreted problem statements differently — and how the organising committee handled such situations during evaluation.

2015 — VSComp 2015: Verification Challenges and Community Response

Venue: Formal Methods Workshop Proceedings

The 2015 report reflects an edition that placed increased emphasis on completeness and documentation. It describes the five problems, the tools used by participants, and includes a section on lessons learned regarding reproducibility. The publication also addresses how the evaluation criteria evolved relative to earlier editions.

2017 — The Verified Software Competition 2017: Challenges in Program Verification

Venue: Conference on Verified Software: Theories, Tools, Experiments

The most recent edition report covers problems that tested concurrent reasoning and refinement techniques alongside traditional assertional verification. It provides a retrospective on the competition series as a whole, discussing trends in tool usage, participation patterns, and the role of the competition in advancing the state of the art in verified software.

Citation and Reference Guidance

If you are citing a VSComp problem or solution in your own research, the publication for the relevant year is the most appropriate reference. A citation should include the competition name, the edition year, the publication title, and the venue. For example: “Verified Software Competition 2014, as reported in [title], published in [venue].”

Where no formal publication exists for a given edition, referencing the competition website with the URL of the specific year page is a reasonable alternative. The solutions archive also notes published reports when they are available, providing a cross-reference between solution entries and the corresponding academic record.

VSComp and the VSTTE Conference Series

Several VSComp publications appeared in the proceedings of VSTTE — Verified Software: Theories, Tools, Experiments. This is not coincidental. The competition was conceived as a practical complement to the research presented at VSTTE, giving participants a concrete arena in which to apply the techniques discussed at the conference. The workshop setting provided a natural venue for presenting competition results and discussing them with the broader community.

Other publications appeared in related formal-methods venues or as standalone technical reports. The diversity of publication venues reflects the interdisciplinary nature of the field: formal verification touches programming languages, software engineering, logic, and mathematics, and the competition reports have found homes in proceedings that span these areas.

Scope of This Page

This page focuses on publications directly produced by or closely associated with the VSComp organising committee. It does not attempt to catalogue every paper that references the competition. Numerous research papers cite VSComp problems as benchmarks for verification tools, and those citations can be found through standard academic search tools.

If you are aware of a publication associated with VSComp that is not listed here, or if you have corrections to the records above, the year pages provide additional context and may include references we have not yet incorporated into this summary.