2016

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

Winners

• Best problem submission: Daniel Grahl, for suggesting "Strassen's algorithm", which inspired the matrix multiplication challenge.
  
• Distinguished user-assistance tool feature: Alexander J. Summers and Malte Schwerhoff (Viper) for their support of quantified permissions.
  
• Best student team (2x): Martin Clochard (Why3), Léon Gondelman & Mário Pereira (Why3)
  
• Best team: Bart Jacobs (VeriFast)

Challenges

DownloadChallenge 1 - Matrix Multiplication (PDF, 69 KB)vertical_align_bottom

DownloadChallenge 2 - Binary Tree Traversal (PDF, 96 KB)vertical_align_bottom

DownloadChallenge 3 - Static Tree Barriers (PDF, 108 KB)vertical_align_bottom

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.

• external pageGidon Ernst (KIV)call_made
• Bart Jacobs (VeriFast): files attached to this page
  
  • Downloadmatmul.java (JAVA, 5 KB)vertical_align_bottom - Challenge 1: Task 1
  • Downloadtree_barrier.java (JAVA, 10 KB)vertical_align_bottom - Challenge 2: all tasks, but not the bonus
  • Downloadtree_traversal.java (JAVA, 4 KB)vertical_align_bottom - Challenge 3: Task 1 

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

• Luca Weibel and Christiaan Dirkx (Dafny) - DownloadChallenge 1 (DFY, 2 KB)vertical_align_bottom attached to this page
• Combined solutions of external pageMartin Clochard (Why3), Léon Gondelman & Mário Pereira (Why3)call_made
• Jan Friso Groote (mCRL2) - DownloadChallenge1.zip (ZIP, 5 KB)vertical_align_bottom, DownloadChallenge2.zip (ZIP, 6 KB)vertical_align_bottom, DownloadChallenge3.zip (ZIP, 246 KB)vertical_align_bottom
  
• Stephen Siegel (CIVL) - Challenge 1: Downloadtask 1 (CVL, 2 KB)vertical_align_bottom, Downloadtask 2 (CVL, 970 Bytes)vertical_align_bottom, Downloadtask 3 (CVL, 5 KB)vertical_align_bottom, DownloadChallenge 2 (CVL, 2 KB)vertical_align_bottom, and DownloadChallenge 3 (CVL, 3 KB)vertical_align_bottom attached to this page, see also Stephen Siegel's external pagepapercall_made in Siglog (volume 4, number 2, April 2017)

The challenges will be published after the event.

RULES

1. Solutions are to be submitted per email.
   
2.  Submissions must state the version of the verification system used (for development versions, internal revision, timestamp, or similar unique id).
3. 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.
4. It is allowed to modify the verification system during the competition. This is to be noted in the solution(s)
5. All techniques used must be general-purpose, and are expected to extend usefully to new unseen problems
6. Internet access is allowed, but using the interget to search for problem solutions is not.
7. Involvement of other people beyond those on the team is not allowed.
8. 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.)