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”.
ATB*BCOMP*Disable_Array_Compatibility_Check:TRUE
ATB*BCOMP*Disable_Concrete_Constants_Type_Check:TRUE
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

Last modified 1yr ago