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