release 1.0

date: 4/16/2004

1. Description

VICS, Verification of an Implementation Conforming to its Specification, aims to check (i.e. not to prove) the correctness of a refinement of the B formal method, between an abstract machine (a formal specification) and its possible implementation [ B Site pages, B-Book]. This tool is based on Mozart.

The context of use of this tool is essentially academic. This tool can be used for programming courses: the correct abstract machine is given by the teacher and the student has to write the corresponding implementation (in B0, a pascal like syntax). The students use this tool to check if their implementations are correct. If not, VICS gives a counter-example.

This project has been proposed on Sourceforge because it needs people to contribute to the development and the documentation.



This project was asked by professor Pierre-Yves Schobbens (FUNDP, Belgium). VICS has been parlty realized by Laïka Moussa during her work experience placement at CETIC, under the direction of Pierre-Yves Schobbens and Emmanuel Dieul. VICS took advantage of Isabelle Dony 's work. More informations can be found (in french) at (report on the conception). Emmanuel Dieul has mainly developed the first public release of VICS.

This tool was presented at:


No documentation is available at the moment, but some could be found in french at


release 1.0
First release

Sources :
vics-1.0.tgz All the source code of VICS and the makefiles. Be sure that you already have installed the Mozart platform before you compile. For compilation, just type "make", and "make test" to run VICS.