Abstraction and Modular Verification of Infinite-State Reactive Systems

Zohar Manna, Michael Colon, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomas Uribe

We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental verification of systems as they are developed and refined. In particular, we show how deductive verification tools, and the combination of finite-state model checking and abstraction, allow the verification of infinite-state systems featuring data types commonly used in software specifications, including real-time and hybrid systems.

Appeared in Requirements Targeting Software and Systems Engineering (RTSE), LNCS 1526, Springer Verlag, pp 273-292, 1998.

Postscript, PDF. © 1998, Springer Verlag.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Thu Mar 29 10:39:10 PST 2001