Problem Catalogue
Every VSComp edition publishes a set of precisely specified verification challenges. This page collects all problems across every competition year into a single browsable catalogue, organised by domain, difficulty, and artifact type.
Anatomy of a VSComp Problem
A VSComp problem is not a conventional programming exercise. Each challenge consists of a formal specification — a precise, mathematical description of the expected behaviour — paired with either a reference implementation or the requirement to produce one. Participants must then provide a machine-checkable proof that the implementation satisfies the specification.
In practice, a typical submission includes three artifacts: annotated source code (with preconditions, postconditions, and loop invariants), a formal specification written in the language of the chosen proof assistant or verification tool, and the proof itself. Some problems additionally require complexity arguments, concurrency proofs, or refinement mappings. The exact requirements vary by problem and are documented in each problem's description.
The difficulty of these challenges comes not from algorithmic complexity in the competitive-programming sense, but from the subtlety of stating and proving the right properties. A sorting routine may seem straightforward until you must formally prove that the output is a permutation of the input, not merely that it is ordered. Similarly, verifying a concurrent data structure demands reasoning about interleavings, atomicity, and memory models that have no analogue in sequential programming.
Domains Represented in the Catalogue
Problems in the catalogue span a range of verification domains. Each domain tests different proof techniques and tool capabilities. The following domains appear across the four competition years:
- Assertional verification — classical Hoare-style reasoning over sequential code, with preconditions, postconditions, and loop invariants.
- Data structures — proving structural invariants of trees, lists, and other linked structures through pointer manipulation.
- Concurrency — verifying thread-safe data structures, lock-free algorithms, and shared-state protocols under concurrent access.
- Refinement — establishing formal relationships between abstract specifications and concrete implementations using simulation or trace inclusion.
- Systems verification — proving properties of realistic software components such as editors, servers, and storage engines.
- Amortized complexity — formally bounding the amortized cost of operations using potential functions or equivalent techniques.
- Hybrid systems — verifying safety properties of controllers that combine continuous dynamics with discrete mode switches.
- Security protocols — proving confidentiality, authentication, or integrity properties under adversary models.
- Specification completeness — meta-level reasoning about whether a specification covers all relevant behaviours.
- Functional correctness — general-purpose correctness proofs for algorithms and compilers.
- Text processing — proving correctness of pattern-matching, parsing, and string-manipulation routines.
Not every domain appears in every year. The years index shows which domains were featured in each edition. For the evaluation approach used to assess submissions, see the rules page.
Use the categories below to orient yourself within the catalogue. Problems are displayed in chronological order by default.
VSComp 2010
Prove that a given sorting algorithm correctly produces a permutation of its input in non-decreasing order. Requires loop invariants, termination arguments, and a clear specification of what it means for the output to be sorted.
Verify that insertion and lookup operations on a binary search tree maintain the BST invariant. Participants must formalise the ordering property and show it is preserved across all operations.
Prove correctness of a partitioning routine that separates an array into elements below and above a pivot value. Classic loop-invariant reasoning with attention to index boundaries.
Verify an in-place reversal of a singly linked list. The challenge lies in specifying and preserving the relationship between the original and reversed sequences through pointer manipulation.
Prove that a linear-time algorithm correctly computes the maximum contiguous subarray sum. Requires careful loop invariant formulation and boundary case reasoning.
VSComp 2014
Verify a lock-free concurrent queue implementation. Participants must show linearisability or an equivalent correctness condition under concurrent access from multiple threads.
Establish a refinement mapping between an abstract specification and a concrete implementation of a stateful component. Demonstrate trace inclusion or simulation.
Verify that a shared monotonic counter maintains its invariant — the counter value never decreases — under concurrent increments. Requires reasoning about atomicity and memory ordering.
Prove the correctness of a priority queue implementation, showing that extraction always returns the minimum element and that the heap property is maintained through all operations.
Show bisimulation equivalence between two state machine specifications. Requires constructing the bisimulation relation and proving it satisfies the transfer conditions.
VSComp 2015
Verify the core operations of a gap-buffer–based text editor: insertion, deletion, and cursor movement. The challenge tests whether verification tools can handle realistic stateful data structures with complex internal invariants.
Verify key components of a simplified DNS resolver, including query parsing, cache lookup, and response construction. Participants must specify the expected behaviour at the network-message level.
Prove both functional correctness and amortized O(1) complexity for a two-stack queue implementation. Requires a potential function argument or equivalent amortized analysis technique formalised in the proof assistant.
Verify append and compaction operations of a simplified log-structured storage engine. Participants must show crash consistency: the data structure remains valid even if an operation is interrupted.
Prove that a string-matching algorithm correctly identifies all occurrences of a pattern within a text. Requires careful index arithmetic and completeness arguments.
VSComp 2017
Verify safety properties of a hybrid controller that alternates between continuous dynamics and discrete mode switches. Participants must formalise the continuous invariant and show it is preserved across mode transitions.
Verify confidentiality and authentication properties of a simplified secure messaging protocol. The specification must account for an active adversary model within stated assumptions.
Given a partial specification of a component, identify missing cases and complete the specification so that no unspecified behaviours remain. This meta-level challenge asks participants to reason about what a specification omits.
Verify a single round of a consensus protocol in a distributed setting with crash faults. Participants must prove agreement and validity properties under the stated fault model.
Prove that a simple compiler optimisation pass preserves the semantics of the source language. Requires defining an operational semantics and showing a simulation relation.
Submitted solutions for these problems are collected in the solutions archive, grouped by year and problem. Each entry describes the verification approach, tools used, and the degree of completeness achieved.
The rules page describes how submissions are evaluated, including the criteria for correctness, completeness, and clarity that reviewers apply to each solution.