A UNITY-based Algorithm Design Assistant
Abdellah El Hadri
In TACAS, pages
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
ENSSEEIHT-IRIT, Toulouse, France and EMI, Rabat, Maroc.
Available as PostScript.
BRICS WWW home page