%0 Conference Proceedings
%F Jard-Jeron-CAV91
%A Jard, C.
%A Jéron, T.
%T Bounded Memory Algorithms for Verification On the fly
%B CAV'91: Symposium on Computer Aided Verification, Aalborg, Denmark
%V 575
%P 192-202
%S LNCS
%I Springer Verlag
%X 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. But for numerous properties, it is not necessary to explicitely build this graph and an exhaustive depth-first traversal is often sufficient. In order to avoid retraversing states, we must then store some already visited states in memory. But since the memory size is bounded, visited states must be randomly replaced. In most cases this depth-first traversal with replacement can push back the limits of verification tools
%U http://www.irisa.fr/vertecs/Publis/Ps/91-CAV.ps.gz
%8 June
%D 1991