View article

The analysis of programs by the exhaustive inspection of reachable states in a finite-state graph is a well-understood procedure. It is straightforwardly applicable to many description languages and is actually implemented in several industrial tools. But one of the main limitations of today's verification tools is the size of the memory needed to exhaustively build the state graphs of the programs. For numerous properties, it is not necessary to explicitly build this graph; an exhaustive depth-first traversal is often sufficient. This leads to an on-line algorithms for computing Büchi acceptance (in the deterministic case) and behavioral equivalences: they are presented in detail. In order to avoid retraversing states, it is, however, important to store some of the already visited states in memory. To keep the memory size bounded (and avoid a performance falling down), visited states are randomly replaced. In most cases …