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.