Verified Software Competitions

Introduction

Several software verification competitions have been organized last years, with different objectives and modalities. Some problems from these competitions have been selected and solved using the B method. For each of these problems, are provided:
  • a B model archive, containing the B models, the proof files (saved demonstration), the added mathematical rules (to be used during interactive proof)
  • a report:
    • explaining how the problem was tackled (possibly with several options), how the proof was conducted,
    • providing project metrics per component
    • showing the generated source code when executed
  • source code, generated by Atelier B from B models and handwritten for others files.
These projects should be replayed with Atelier B 4.1 or greater with the parameters below. Copy the two lines, select your Atelier B project, open contextual menu, select โ€œpropertiesโ€ then โ€œresources fileโ€, paste the two lines at the end of the file, press โ€œOKโ€.
1
ATB*BCOMP*Disable_Array_Compatibility_Check:TRUE
2
ATB*BCOMP*Disable_Concrete_Constants_Type_Check:TRUE
Copied!

VSTTE 2010

The VSTTE 2010 conference was organized August 16-19, 2010 in Edinburgh, Scotland (website). Problems are available here.

Problem 1: Sum and maximum

โ€œGiven an N-element array of natural numbers, write a program to compute the sum and the maximum of the elements in the array.โ€
Report
Problem_11.pdf
622KB
PDF
B Projet Archive
VSTTE10_1_B.arc
27KB
Binary
Source code
vstte10_1_code.zip
4KB
Binary

Problem 2: Inverting an injection

โ€œInvert an injective array A on N elements in the subrange from 0 to N-1, i.e. the output array B must be such that B[A[i]] = i for 0 โ‰ค i ห‚ N. You can assume that A is surjective.โ€
Report
Problem21.pdf
610KB
PDF
B Projet Archive
VSTTE10_2_B.arc
13KB
Binary
Source code
vstte10_2_code.zip
2KB
Binary

Problem 3: Searching a Linked List

โ€œGiven a linked list representation of a list of integers, find the index of the first element that is equal to 0.โ€
Report
Problem31.pdf
622KB
PDF
B Projet Archive
VSTTE10_3.arc
14KB
Binary
Source code
vstte10_3_code.zip
10KB
Binary

Problem 4: N-Queens

โ€œWrite a program to place N queens on an N*N chess board so that no queen can capture another one with a legal move.โ€
Report
Problem_4.pdf
653KB
PDF
B Projet Archive
NQueens_eventB.arc
5KB
Binary
Rodin Project Archive
NQueens.zip
65KB
Binary

VSTTE 2011

The COST IC701 Verification Competition 2011 was organized at the occasion of the conference on Formal Verification of Object-Oriented Software, held in 5-7 October, 2011, at Turin, Italy (website). Problems are not available any more from the website.

Challenge 3: Two equal elements

โ€œGiven an integer array A of length n+2 with n>=2. It is known that at least two values stored in the array appear twice (i.e., there are at least two duplets). Implement and verify a program finding such two values. You may assume that the array contains values between 0 and n-1.โ€œ
Report
Challenge_32.pdf
725KB
PDF
B Projet Archive
COST_3_B.arc
27KB
Binary
Source code
COST_3_code.zip
3KB
Binary

VSTTE 2012

The VSTTE 2012 conference was organized January 28-29, 2012 in Philadelphia, USA (website). Problems are available here.

Problem 1: Two-way sort

โ€œWe want to sort an array of Boolean values (assuming false < true) using only swaps.โ€
Report
Problem_11.pdf
622KB
PDF
B Projet Archive
VSTTE12_1_B.arc
30KB
Binary
Source code
vstte12_1_code.zip
4KB
Binary

Problem 3: Ring Buffer

โ€œWe want to implement a queue data structure using a ring buffer.โ€
Report
Challenge-3.pdf
781KB
PDF
B Projet Archive
VSTTE12_3_B.arc
52KB
Binary
Source code
vstte12_3_code.zip
25KB
Binary