[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

some questions

Hi all,

I have some questions concerning the model-checker in PVS.

One big difference between the PVS model checker and other checkers like
SMV is that PVS does not (yet) generate a counterexample path when a
property does not hold in a model. Some papers (like "an integration of
model checking with automated proof checking") mention that the generation
of such paths will be investigated. Is there already progress since
it is very interesting to have the counterexample paths (must easier do
find the main reason of the failure).

Beside that, it seems that the model checker also can verify properties
very slow. Do I have to look for this problem in my specification or
are there also other reasons (lazy implementation, ...)? Can anyone
comment on this?

Thanks a lot for the answers,