Solutions

This page contains links to the solutions developed by participants during the competition, and polished afterwards. Solutions may be updated as time goes on.

Gidon Ernst (KIV)
Bart Jacobs (VeriFast): files attached to this page

matmul.java - Challenge 1: Task 1
tree_barrier.java - Challenge 2: all tasks, but not the bonus
tree_traversal.java - Challenge 3: Task 1

See also Bart Jacob's paper in the proceedings of FTfJP 2016.

Luca Weibel and Christiaan Dirkx (Dafny) - Challenge 1 attached to this page
Combined solutions of Martin Clochard (Why3), Léon Gondelman & Mário Pereira (Why3)
Jan Friso Groote (mCRL2) - Challenge1.zip, Challenge2.zip, Challenge3.zip attached to this page
Stephen Siegel (CIVL) - Challenge 1: task 1, task 2, task 3, Challenge 2, and Challenge 3 attached to this page, see also Stephen Siegel's paper in Siglog (volume 4, number 2, April 2017)