RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

More precisely, we used the new functional containers that will be part of the next release of SPARK to specify the behavior of memory allocators, which are implemented in terms of arrays. We use ghost code to define the link between abstract specification and concrete implementation, in two different ways:

1. In the simpler case, a ghost function provides an abstract view of the concrete implementation.
2. In the more complex case, a ghost variable is defined to evolve the model together with the concrete data.

This interesting experiment showed us that the kind of refinement proofs that were usual in the B method, for example, are also applicable in SPARK. And that complete automation of proof is achievable in such cases too.

The conference takes place in Paris from June 28 to June 30. For the complete conference program, see here. The full article we wrote is attached.