Training Resources for Atelier B

Searchβ¦

Getting Your Hands Dirty

Event-B Examples

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

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

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