2019

verifyThis 2019 was organized by Claire Dross, Carlo A. Furia

The competition report can be found Downloadhere (PDF, 285 KB)

Challenges

Challenge 1
DownloadMonotonic Segments and GHC sort (PDF, 136 KB)

Challenge 2
DownloadCartesian Trees (PDF, 137 KB)

Challenge 3
DownloadSparse Matrix Multiplication (PDF, 116 KB)

Solutions

Sample solutions by the organizers, Downloadchallenge 1 (ZIP, 3 KB), Downloadchallenge 2 (ZIP, 5 KB), Downloadchallenge 3 (ZIP, 2 KB)

Mergesort: Quentin Garchery, Downloadchallenge 1, Downloadchallenge 2, Downloadchallenge 3

VerCors T(w/o)o: Marieke Huisman, Sebastiaan Joosten, external pagesolutions

Bashers: Mohammad Abdulaziz, Maximilian P L Haslbeck

Jourdan-Mével: Jacques-Henri Jourdan, Glen Mével, Downloadchallenge 1 (V, 6 KB) Downloadchallenge 2 (V, 4 KB), Downloadchallenge 3 (V, 6 KB)

OpenJML: David Cok, Downloadchallenge 1 (JAVA, 4 KB), Downloadchallenge 2 (JAVA, 3 KB)

YVeTTe: Virgile Prevosto, Virgile Robles, external pagesolutions

The Refiners: Peter Lammich, Simon Wimmer, Downloadsolutions

KIV: Stefan Bodenmüller, Gerhard Schellhorn, external pagesolutions

Sophie & Wytse: Sophie Lathouwers, Wytse Oortwijn, external pagesolutions

Coinductive Sorcery: Jasper Hugunin, Downloadchallenge 1 (V, 4 KB), Downloadchallenge 2 (V, 5 KB), Downloadchallenge 3 (V, 6 KB)

Heja mig: Christian Lidström

Eindhoven University of Technology, Formal Systems Analysis: Jan Friso Groote, Thomas Neele, Downloadchallenge 1 (ZIP, 2 KB), Downloadchallenge 2 (ZIP, 1 KB), Downloadchallenge 3 (ZIP, 3 KB)

Viper (ETH Zurich): Alexander J. Summers, Downloadchallenge 1 (VPR, 3 KB), Downloadchallenge 2 (VPR, 5 KB), Downloadchallenge 3 (VPR, 11 KB)

Prizes

Best overall team
The Refiners (Simon Wimmer and Peter Lammich)

Most distinguished tool feature (two awards)
The Bashers (Mohammad Abdulaziz and Maximilian P L Haslbeck) for a library to model concurrency in Isabelle, which they developed specifically in preparation for the competition.
VerCors T(w/o)o (Sebastiaan Joosten and Marieke Huisman) for their usage of ghost method parameters to model sparse matrices.

Best student team (two awards)
Mergesort (Quentin Garchery)
Sophie & Wytse (Sophie Lathouwers and Wytse Oortwijn)

Tool used by most teams
Viper (Alexander J. Summers) used directly or indirectly by three teams