2014

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

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

Challenge

verifyThis 2014 was held as part of a Dagstuhl seminar on external pageEvaluating 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.

DownloadChallenge (PDF, 39 KB)

Downloadbubble_sort_list_buggy.c (C, 4 KB)

Downloadbubble_sort_list_fixed.c (C, 4 KB)