What if Model Checking Must be Truly Symbolic?
In TACAS, pages
There are many methodologies whose main concern it is to reduce
the complexity of a verification problem to be ultimately able to apply model
checking. Here we propose to use a model checking like procedure which
operates on a small, truly symbolic description of the model. We do so by
exploiting systematically the separation between the (small) control part and
the (large) data part of systems which often occurs in practice. By expanding
the control part, we get an intermediate description of the system which
already allows our symbolic model checking procedure to produce meaningful
results but which is still small enough to allow model checking to be
Oldenburg, Germany and Haifa, Israel.
Available as PostScript,
BRICS WWW home page