Introduction to generalized symbolic trajectory evaluation

Symbolic trajectory evaluation (STE) is a lattice-based model checking technology based on a form of symbolic simulation. It offers an alternative to ´classical´ symbolic model checking that, within its domain of applicability, often is much easier to use and much less sensitive to state explosion. The limitation of STE, however, is that it can only express and verify properties over finite time intervals. In this paper, we present a generalized STE (GSTE) that extends STE style model checking to properties over infinite time intervals. We further strengthen the power of GSTE by introducing a form of backward symbolic simulation. It can be shown that these extensions, together with a notion of fairness, give STE the power to verify all ω-regular properties. We use a large-scale industrial memory design to demonstrate the power and practicality of GSTE