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

Re: some questions




Sara:
  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.

-Shankar

> From:    Sara Van Langenhove <svlangen@cage.ugent.be>
> Subject: some questions
> Date:    Fri, 29 Aug 2003 15:52:22 +0200 (CEST)
> To:      support PVS <pvs-help@csl.sri.com>
> 
> 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,
> 
> Greetz,
> 
> Sara
>