2019
verifyThis 2019 was organized by Claire Dross, Carlo A. Furia
The competition report can be found Download here (PDF, 285 KB)
Challenges
Challenge 1
Download Monotonic Segments and GHC sort (PDF, 136 KB)
Challenge 2
Download Cartesian Trees (PDF, 137 KB)
Challenge 3
Download Sparse Matrix Multiplication (PDF, 116 KB)
Solutions
Sample solutions by the organizers, Download challenge 1 (ZIP, 3 KB), Download challenge 2 (ZIP, 5 KB), Download challenge 3 (ZIP, 2 KB)
Mergesort: Quentin Garchery, Download challenge 1, Download challenge 2, Download challenge 3
VerCors T(w/o)o: Marieke Huisman, Sebastiaan Joosten, external page solutions
Bashers: Mohammad Abdulaziz, Maximilian P L Haslbeck
Jourdan-Mével: Jacques-Henri Jourdan, Glen Mével, Download challenge 1 (V, 6 KB) Download challenge 2 (V, 4 KB), Download challenge 3 (V, 6 KB)
OpenJML: David Cok, Download challenge 1 (JAVA, 4 KB), Download challenge 2 (JAVA, 3 KB)
YVeTTe: Virgile Prevosto, Virgile Robles, external page solutions
The Refiners: Peter Lammich, Simon Wimmer, Download solutions
KIV: Stefan Bodenmüller, Gerhard Schellhorn, external page solutions
Sophie & Wytse: Sophie Lathouwers, Wytse Oortwijn, external page solutions
Coinductive Sorcery: Jasper Hugunin, Download challenge 1 (V, 4 KB), Download challenge 2 (V, 5 KB), Download challenge 3 (V, 6 KB)
Heja mig: Christian Lidström
Eindhoven University of Technology, Formal Systems Analysis: Jan Friso Groote, Thomas Neele, Download challenge 1 (ZIP, 2 KB), Download challenge 2 (ZIP, 1 KB), Download challenge 3 (ZIP, 3 KB)
Viper (ETH Zurich): Alexander J. Summers, Download challenge 1 (VPR, 3 KB), Download challenge 2 (VPR, 5 KB), Download challenge 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