Programming Methodology Group

Search

en

2017

verifyThis 2017 was organized by Wojciech Mostowski, Mattias Ulbrich

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

DownloadChallenge Sheet (PDF, 88 KB)

DownloadPseudocode (PDF, 35 KB)

external pageLink 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.

DownloadChallenge Sheet (PDF, 87 KB)

Challenge 3: 14.00 - 15.30

DownloadChallenge Sheet (PDF, 87 KB)

Challenge 4: 16.00 - 17.30

DownloadChallenge Sheet (PDF, 92 KB)

Solutions

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

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

3. Lionel Blatter, Jean-Christophe Léchenet (Frama-C) 
Downloadsolution challenge 1 (C, 5 KB), Downloadaddendum (PDF, 8 KB) to solution challenge 1,
updated solution Downloadchallenge 1 (C, 9 KB)
Downloadsolution challenge 2 (C, 3 KB), updated solution Downloadchallenge 2 (C, 3 KB)
Downloadsolution challenge 3 (C, 3 KB)
solution challenge 4 (Downloadcoq (V, 3 KB), DownloadFrama_C (C, 2 KB))

4. Mihai Herda (KeY)
Downloadsolution challenge 1 (JAVA, 3 KB)
solution challenge 2 (Download1 (JAVA, 2 KB), Download2 (PROOF, 266 KB), Download3 (PROOF, 103 KB))
Downloadsolution challenge 3 (JAVA, 2 KB)

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

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

7. Marieke Huisman, Wytse Oortwijn (VerCors)
Downloadsolution challenge 1 (PVL, 3 KB)
solution challenge 2 (Downloada (PVL, 2 KB), Downloadb (PVL, 1 KB)) Downloadcomment (TXT, 142 Bytes)
Downloadsolution challenge 4 (PVL, 3 KB)

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

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

10. Mário Pereira, Raphael Rieu-Helft  (Why3)
Downloadsolution challenge 1 (MLW, 2 KB)
Downloadsolution challenge 3 (MLW, 4 KB),
updated solution Downloadchallenge 3 (MLW, 5 KB)
Downloadsolution 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.)

 

JavaScript has been disabled in your browser