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