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

Re: another question

  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.


> 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