Visual Verification of Reactive Systems

Luca de Alfaro, Zohar Manna, Henny Sipma, Tomas Uribe

We describe diagram-based formal methods for verifying temporal properties of finite- and infinite-state reactive systems. These methods, which share a common background and tools, differ in the way they use automatic procedures within an interactive setting based on deduction. They can be used to produce a static proof object, or to perform incremental analysis of systems and specifications.

Appeared in Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer-Verlag, 1997.

Postscript, PDF. © 1997, Springer Verlag.

© Henny Sipma /
Last modified: Thu Mar 29 17:37:37 PST 2001