VerifyThis 2017

verifyThis 2017 was organized by Wojciech Mostowski, Mattias Ulbrich

The competition report can be found 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

• Challenge Sheet (PDF, 88 KB)
• Pseudocode (PDF, 35 KB)
• 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.

Challenge Sheet (PDF, 87 KB)

Challenge 3: 14.00 - 15.30

Challenge Sheet (PDF, 87 KB)

Challenge 4: 16.00 - 17.30

Challenge Sheet (PDF, 92 KB)

Solutions

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

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

3. Lionel Blatter, Jean-Christophe Léchenet (Frama-C) solution challenge 1 (C, 5 KB), addendum (PDF, 8 KB) to solution challenge 1, updated solution challenge 1 (C, 9 KB) solution challenge 2 (C, 3 KB), updated solution challenge 2 (C, 3 KB) solution challenge 3 (C, 3 KB) solution challenge 4 (coq (V, 3 KB), Frama_C (C, 2 KB))

4. Mihai Herda (KeY) solution challenge 1 (JAVA, 3 KB) solution challenge 2 (1 (JAVA, 2 KB), [2 (PROOF, 266 KB)](solutions/KEYchallenge2.Sort(challenge2.Sort__sort((I)).JML%20normal_behavior%20operation%20contract.0.proof), 3 (PROOF, 103 KB) solution challenge 3 (JAVA, 2 KB)

5. Michael Kirsten, Jonas Schiffl (KeY) solution challenge 1 (JAVA, 2 KB) (signature (ASC, 836 Bytes)),updated solution challenge 1 (GZ, 1.4 MB), signature (ASC, 834 Bytes), solution challenge 3 (JAVA, 3 KB) (signature (ASC, 836 Bytes), comment (TXT, 408 Bytes)) solution challenge 4 (JAVA, 3 KB) (signature (ASC, 836 Bytes))

6. Stefan Bodenmüller, Jörg Pfähler (KIV) solution challenge 1 solution challenge 2 (TXT, 389 Bytes) completed and updated solution for all challenges

7. Marieke Huisman, Wytse Oortwijn (VerCors) solution challenge 1 (PVL, 3 KB) solution challenge 2 (a (PVL, 2 KB), b (PVL, 1 KB)) comment (TXT, 142 Bytes) solution challenge 4 (PVL, 3 KB)

8. Jean-Christophe Filliâtre (Why3) solution challenge 1 (MLW, 4 KB), comment (TXT, 156 Bytes), solution challenge 2 (MLW, 4 KB), comment challenge2 (TXT, 438 Bytes) solution challenge3 (MLW, 6 KB) (Kadane_2d (MLW, 3 KB)) comment (TXT, 471 Bytes)
   solution challenge 4 (MLW, 4 KB) (comment (TXT, 374 Bytes))\

9. Léon Gondelman, Marc Schoolderman (Why3)
   solution challenge 1 (MLW, 2 KB), (comment (TXT, 358 Bytes))
   solution challenge 2 (MLW, 2 KB), (comment (TXT, 131 Bytes))
   solution challenge 3 (MLW, 2 KB) (comment (TXT, 97 Bytes))

10. Mário Pereira, Raphael Rieu-Helft (Why3)
    solution challenge 1 (MLW, 2 KB)
    solution challenge 3 (MLW, 4 KB),
    updated solution challenge 3 (MLW, 5 KB)
    solution challenge 4 (MLW, 3 KB)

Rules

Solutions are to be submitted per email to

1. Submissions must state the version of the verification system used (for development versions, internal revision, timestamp, or similar unique id).
2. 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.
3. It is allowed to modify the verification system during the competition. This is to be noted in the solution(s)
4. All techniques used must be general-purpose, and are expected to extend usefully to new unseen problems
5. Internet access is allowed, but using the interget to search for problem solutions is not.
6. Involvement of other people beyond those on the team is not allowed.
7. 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.)