VerifyThis 2014

verifyThis 2014 was organized by Dirk Beyer, Marieke Huisman, Vladimir Klebanov, Rosemary Monahan.

The competition report can be found here (PDF, 1.1 MB).

Challenge

verifyThis 2014 was held as part of a Dagstuhl seminar on Evaluating Software Verification Systems:Benchmarks and Competitions.

Challege 1: Conincidence Count

The first challenge was part of a Dafny tutorial: Given 2 integer arrays in strictly increasing order, find the number of values occurring in both sequences (Coincidence Count, A Method of Programming, Dijkstra & Feijen)

Challege 2: Bubblesort for Doubly-Linked Lists

This challenge is based on a real bug encountered in the Linux kernel source.

• Challenge (PDF, 39 KB)
• bubble_sort_list_buggy.c (C, 4 KB)
• bubble_sort_list_fixed.c (C, 4 KB)