> For the complete documentation index, see [llms.txt](https://b-method.gitbook.io/training-resources-for-atelier-b/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://b-method.gitbook.io/training-resources-for-atelier-b/examples-and-case-studies/verified-software-competitions.md).

# 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](https://sites.google.com/site/vstte2012/call-for-papers)). Problems are available [here](https://www.cs.utexas.edu/users/moore/acl2/vstte-2012/problems.pdf).

### 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     

{% file src="/files/XqxBW6EswV3Un7eNR2Hd" %}

B Projet Archive  

{% file src="/files/UPIZ4yBCMnDFaMROWvmo" %}

Source code

{% file src="/files/R8eqFKNRXMWTGGRnz3C9" %}

### 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     

{% file src="/files/Hqa3eplgPrCaUS4LrN6g" %}

B Projet Archive     

{% file src="/files/bin5uj2K7ZeY2ShSR8SA" %}

Source code

{% file src="/files/Ll6kSKkYbFULiqTe8nQT" %}

### 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     

{% file src="/files/3jVmPFgdYVLCXUqsJY3H" %}

B Projet Archive     

{% file src="/files/cR0ZuUNL7O2NZC8t3FR6" %}

Source code

{% file src="/files/vtJHVpyJ43hNzsBiLwBB" %}

### 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    

{% file src="/files/FR3cklcykrz24g5ayOBR" %}

B Projet Archive     

{% file src="/files/4H0CtDn8eaRWBLZKRisn" %}

Rodin Project Archive

{% file src="/files/LPByCep8pUpzGd0VLRwf" %}

## 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](http://foveoos2011.cost-ic0701.org/verification-competition)). 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        

{% file src="/files/LoOlJ7YFZL7By1qs5xQ3" %}

B Projet Archive     

{% file src="/files/WpMuBCyNCdL6Ji55cmmM" %}

Source code

{% file src="/files/rQCcrDpccPGPJo7lxLFj" %}

## VSTTE 2012

The VSTTE 2012 conference was organized January 28-29, 2012 in Philadelphia, USA ([website](https://sites.google.com/site/vstte2012/call-for-papers)). Problems are available [here](https://www.cs.utexas.edu/users/moore/acl2/vstte-2012/problems.pdf).

#### Problem 1: Two-way sort

“*We want to sort an array of Boolean values (assuming false < true) using only swaps.*”

Report       &#x20;

{% file src="/files/bjlrErI6FXaLOKatKBpW" %}

B Projet Archive    &#x20;

{% file src="/files/dr8E0majZ02YSQ90xdXW" %}

Source code

{% file src="/files/OscEkjScAKPRcrCRk2je" %}

### Problem 3: Ring Buffer

“We want to implement a queue data structure using a ring buffer.”

Report       &#x20;

{% file src="/files/sq7UdLO7fIHhE2bz8jlW" %}

B Projet Archive    &#x20;

{% file src="/files/nSVaXnhsa5umemDhFpzJ" %}

Source code

{% file src="/files/bGUMjfVzE72S1eU4QCv5" %}