2017

verifyThis 2017 was organized by Wojciech Mostowski, Mattias Ulbrich

The competition report can be found Download here (PDF, 478 KB)

Winners

Best Student Team: Joint winners
Tool: KIV
PhD Students: Jörg Pfähler & Stefan Bodenmüller, University of Augsburg
Tool: Why3
PhD Students: Mario Parreira Pereira & Raphael Rieu-Helft, LRI, Université Paris-Sud.

Best Overall Team:
Tool: Why3
Jean-Christophe Filliâtre, CNRS

Distinguished user-assistance tool feature:
Tool: CIVL
Feature: Comparison of two programs for functional equivalence
Stephen Siegel, University of Delaware

Best Challenge Submitted:
Radu Grigore, University of Kent
Tree Buffer Challenge, Based on his paper in CAV 2015

Challenges

The competition will offer a number of challenges presented in natural language and pseudo code.

Competition Challenges

Challenge 1: 11.00 - 12.30

Download Challenge Sheet (PDF, 88 KB)

Download Pseudocode (PDF, 35 KB)

external page Link to the JDK implementation

Additional Challenge:

In case you end up bored, here is a followup to the Why3-Challenge from Jean-Christophe's presentation: Let's go 2-dimensional.

Download Challenge Sheet (PDF, 87 KB)

Challenge 3: 14.00 - 15.30

Download Challenge Sheet (PDF, 87 KB)

Challenge 4: 16.00 - 17.30

Download Challenge Sheet (PDF, 92 KB)

Solutions

1. Stephen Siegel (CIVL)
Download solution challenge 1 (TXT, 6 KB), updated solution Download challenge 1 (CVL, 2 KB)
Download solution challenge 3 (TXT, 10 KB)
Download solution challenge 4 (TXT, 7 KB)

2. Jon Mediero Iturrioz (Dafny)
Download solution challenge 1 (TXT, 1 KB)
Download solution challenge2 (TXT, 2 KB),
Download solution challenge 3 (TXT, 2 KB)

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.)