A UNITY-based Algorithm Design Assistant

Michel Charpentier
Gérard Padiou
Abdellah El Hadri

In TACAS, pages 131--145

Abstract:

We address the problem of the automatic verification of reactive systems. For such algorithms, parallelism, non-determinism and distribution, lead to frequent design flaws and make debugging difficult. Proving programs with respect to their specification may solve both these problems. In this framework, we describe the implementation of an algorithm design assistant based upon the UNITY formalism. A theorem prover and a Presburger formulas calculator are used to perform the underlying proofs. We illustrate the main difficulties encountered with representative examples.

Comments
ENSSEEIHT-IRIT, Toulouse, France and EMI, Rabat, Maroc.

Available as PostScript.

BRICS WWW home page