The VerifyThis verification competition is a regular event run as an onsite meeting with workshop character in which three challenges are proposed that participants have to verify in 90 minutes each using their favourite program verification tool.
VerifyThis is a series of program verification competitions, which has taken place annually since 2011 (with the exception of 2020). Previous competitions in the series have been held at FoVeOOS 2011, FM 2012, Dagstuhl (April 2014), and ETAPS 2015—2024.
The aims of the competition are:
The competition offers a number of challenges presented in natural language and pseudo code. 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. The correctness properties posed in problems will have the input-output behavior of programs in focus. Solutions will be judged for correctness, completeness, and elegance.
VerifyThis Long-Term Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort on a large scale in a collaborative manner.
The current challenge is dedicated memcached, a simple LRU-cache based key-value server. Memcached is the backbone for fast response times in distributed web-application. The goal is not only to provide an investigation on the server alone, but also take the client-side and the protocol into our considerations.