Re: [Smtcomp-discussion] FP demo track at SMT-COMP
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Tjark W. <tja...@it...> - 2015-06-11 08:15:28
|
On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote: > On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > > Fixing one return value while existing IEEE-compliant implementations > > return different values would be actively harmful in my opinion. It is > > foreseeable then that users will use fp.min to model IEEE min, that > > some (if not most) will be unaware of the subtle semantic difference, > > and that they will ultimately believe they've verified their code when > > it may well break on some architectures. > > I agree with you but note that there is a counter-argument that in the > situation you give, the current semantics will give spurious > counter-examples that cannot be executed on the target platform. I > guess it is personal taste depending on whether you feel it is better to > under or over approximate the behaviour of the system. My reasoning was > that all IEEE-754 compliant systems should be model of the theory. You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely. Best, Tjark |