[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: some questions
You are right on both counts. The PVS model checker is
not particularly fast nor does it produce counterexamples, but
we are working to remedy this. A future version of PVS will
contain a symbolic model checker built by my colleague Leonardo de Moura
that is competitive with the best ones in the market,
and with a general counterexample capability developed
by Maria Sorea and myself. We hope to have this available in
PVS by the end of 2003.
> From: Sara Van Langenhove <email@example.com>
> Subject: some questions
> Date: Fri, 29 Aug 2003 15:52:22 +0200 (CEST)
> To: support PVS <firstname.lastname@example.org>
> 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,