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

Re: another question




Sara:
  That should not be possible.  The abstraction is sound in the
sense that the abstract theorem implies the concrete one, but
not necessarily complete since the abstraction can lose information.

-Shankar

> From:    Sara Van Langenhove <Sara.VanLangenhove@rug.ac.be>
> Subject: another question 
> Date:    Tue, 8 Apr 2003 17:25:14 +0200 (MEST)
> To:      support PVS <pvs-help@csl.sri.com>
> 
> Hi,
> 
> Just a question of interest. Could it be possible to define an abstraction
> which yields to false proofs with the model-checker? (some theorem is true
> in an abstract state space but the theorem is definitely wrong in the
> concrete state space). Is there also a reason for it?
> 
> Thx,
> 
> Sara