Re: [Rodin-b-sharp-user] Adding invariants to an abstract machine (update)

[Matthias S. <Mat...@in...>]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Jeremy,

> My understanding from the discussion that went on at the time was that the bug in question 
> was fairly  well hidden, and that it required some ingenuity to exploit.   This seems like 
> a very high ratio.   Is this the sort of ratio that you would expect?

The bug was indeed difficult to exploit. The underlying inference rule
is however frequently used. Finding out whether a rule application is
sound is undecidable. Hence, the fix does not only affect unsound rule
applications but (almost?) all applications. Therefore you experience a
high ratio of broken proofs.

- -Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFL9Q+BczhznXSdWggRAnWBAJ9K7DgNJ84TzWozgPcRfOQl/MgEjgCfVJ5P
idVR07bl/2lf8O28yI6UReI=
=U52j
-----END PGP SIGNATURE-----