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.

Key words: Program verification, reactive programs, UNITY formalism, parallelism, distribution, theorem proving.


Michel Charpentier <>
Last modified: Thu Feb 10 13:36:55 EST 2000