Zohar Manna
Computer Science Department - Stanford University
Stanford, CA 94305 USA
FAX: (650) 725-4671
manna@cs.stanford.edu
http://theory.stanford.edu/people/zm/home.html
Abstract
Verification Diagrams combine deductive ("theorem-proving") and algorithmic ("model-checking") verification to establish general temporal-logic properties of infinite-state reactive systems. The diagram serves as an abstraction of the system, while its underlying w-automaton represents the desired temporal behavior.
Last Updated: April 13 March, 2000 by Elisabetta Ferrando