2018
verifyThis 2018 was organized by Andrei Paskevich, Gidon Ernst
The competition report can be found Downloadhere (PDF, 512 KB)vertical_align_bottom
Winners
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
Tutorial Information (software)
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:
Exercise 1
Exercise 2
Exercise 3
Solutions
Raphael Rieu (Why 3) Downloadsolutions (GZ, 49 KB)vertical_align_bottom
Wytse Oortwijn and Mohsen Safari (VerCors), external pageGap Buffercall_made, external pageColored Tilescall_made
Rules
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.)