Call for Problems

Get involved even if you cannot participate in the competition: provide a challenge!

ABOUT THE COMPETITION

VerifyThis 2027 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2027) on 10 and 11 April 2027. It is the 15th event in the VerifyThis competition series. Information on previous events and participants can be found at https://verifythis.github.io.

The aims of the competition are:

• to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion.
• to evaluate the usability of program verification techniques and tools.

The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. Solutions will be judged for correctness, completeness and elegance.

CALL FOR PROBLEMS

Coming soon!

ORGANIZERS

• Mário Pereira, NOVA University Lisbon, Portugal
• Neea Rusch, Uppsala University, Sweden

STEERING COMMITTEE

• Marieke Huisman, University of Twente, the Netherlands
• Rosemary Monahan, Maynooth University Maynooth, Ireland
• Peter Müller, ETH Zurich, Switzerland
• Mattias Ulbrich, Karlsruhe Institute of Technology, Germany

Archive

Contributors are encouraged to look at the archive of previous problems or here:

• 2026:
  • Ada and her papers (PDF, 130 KB)
  • Particle simulation (PDF, 192 KB)
  • Multi-Level Page Tables (PDF, 461 KB)
• 2025:
  • Minimum Excludant (PDF, 126 KB)
  • Linus Torvald’s Elegant Linked-List Removal (PDF, 118 KB)
  • Persistent Arrays (PDF, 150 KB)
  • Persistent Disjoint Sets (PDF, 161 KB)
• 2024:
  • The Rope Data Structure (PDF, 131 KB)
  • Smart Array Copy by Shuffled Subsegments (PDF, 137 KB)
  • Work-Stealing for Task Trees (PDF, 145 KB)
• 2023:
  • List Reversal (PDF, 48 KB)
  • Binary Decision Diagrams (PDF, 126 KB)
  • Nonblocking Concurrent Queue using LL/SC Synchronization (PDF, 95 KB)
• 2022:
  • Downsampling a Point Cloud (PDF, 131 KB)
  • Mergesort with Runs (PDF, 121 KB)
  • The World’s Simplest Lock-Free Hash Set (PDF, 125 KB)
• 2021:
  • Lexicographic Permutations (PDF, 105 KB)
  • DLL to BST (PDF, 204 KB)
  • Shearsort (PDF, 123 KB)
• 2020: no verifythis onsite event
• 2019:
  • Monotonic Segments and GHC sort (PDF, 136 KB)
  • Cartesian Trees (PDF, 137 KB)
  • Sparse Matrix Multiplication (PDF, 116 KB)
• 2018:
  • Array Based Queuing Lock
  • Colored tiles
  • Gap buffer
  • Register allocation
• 2017:
  • Pair Insertion Sort (PDF, 88 KB)
  • Maximum-sum subarray (PDF, 87 KB)
  • Odd-even Transposition Sort (PDF, 87 KB)
  • Tree Buffer (PDF, 92 KB)
• 2016:
  • Matrix Multiplication (PDF, 69 KB)
  • Binary Tree Traversal (PDF, 96 KB)
  • Static Tree Barriers (PDF, 108 KB)
• 2015:
  • RELAXED PREFIX (PDF, 40 KB)
  • Parallel GCD (PDF, 39 KB)
  • Dancing Links (PDF, 37 KB)
• 2014:
  • The first challenge was part of a Dafny tutorial: Given 2 integer arrays in strictly increasing order, find the number of values occurring in both sequences (Coincidence Count, A Method of Programming, Dijkstra & Feijen)
  • This challenge is based on a real bug encountered in the Linux kernel source. Challenge (PDF, 39 KB)
• 2012:
  • LCP (ZIP, 2 KB)
  • Prefix Sum (ZIP, 67 KB)
  • Tree Deletion (ZIP, 731 Bytes)
• 2011:
  • Finding the Maximum in an Array (txt, 917 B)
  • Finding the Maximum in a Tree (txt, 614 B)
  • Finding Two Duplets in an Array (txt, 581 B)
  • Deciding Cyclicity of a List (txt, 360 B): for teams to address outside the competition