What if Model Checking Must be Truly Symbolic?

Werner Damm
Hardi Hungar
Orne Grumberg

In TACAS, pages 230--244

Abstract:

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 performed.

Comments
Oldenburg, Germany and Haifa, Israel.

Available as PostScript, DVI.

BRICS WWW home page