verifyThis 2018 was organized by Andrei Paskevich, Gidon Ernst.
The competition report can be found here (PDF, 512 KB)
Overall Best Team Peter Lammich and Simon Wimmer (Isabelle, TU Munich)
Student Gold Medal Raphaël Rieu-Helft (Why3, Inria)
Student Team Silver Medal Wytse Oortwijn and Mohsen Safari (VerCors, Twente)
Distinguished Tool Feature Jörg Pfähler and Stefan Bodenmüller (Augsburg) for their program refinement method in KIV
Best Challenge Submitted Jean-Christophe Filliâtre, Colored Tiles
VerifyThis 2018 includes an interactive tutorial using the Viper verification tools. If you would like to follow the tutorial using your own copy of the tools, please see the installation instructions here.
A (slower) online version of the tools is also available.
The short exercises for you to try during the tutorial can be found here:
Raphael Rieu (Why 3) solutions (GZ, 49 KB)
Wytse Oortwijn and Mohsen Safari (VerCors), Gap Buffer, Colored Tiles
Solutions are to be submitted per email to
Submissions must state the version of the verification system used (for development versions, internal revision, timestamp, or similar unique id). The main rule of the competition is no cheating is allowed. The judges may penalize or disqualify entrants in case of unfair competition behavior and may adjust the competition rules to prevent future abuse. It is allowed to modify the verification system during the competition. This is to be noted in the solution(s) All techniques used must be general-purpose, and are expected to extend usefully to new unseen problems Internet access is allowed, but using the interget to search for problem solutions is not. Involvement of other people beyond those on the team is not allowed. While care is taken to ensure correctness of the reference implementations supplied with problem descriptions, the organizers do not guarantee that they are indeed correct.
(We acknowledge Geoff Sutcliffe for inspiring/suggesting some of these rules.)