Getting Your Hands Dirty

B Training Course

Event-B Examples

Verified Software Competitions

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

β*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

β*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

β*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

β*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

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.

β*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

β*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

β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 7mo ago

Copy link

On this page

Introduction

VSTTE 2010

Problem 1: Sum and maximum

Problem 2: Inverting an injection

Problem 3: Searching a Linked List

Problem 4: N-Queens

VSTTE 2011

VSTTE 2012

Problem 3: Ring Buffer