4 ms·

Anybody used it? I attended the lecture "introduction to formal methods" by one of the profs behing the project at KIT. It was a fantastic lecture and the prof

Anybody used it? I attended the lecture "introduction to formal methods" by one of the profs behing the project at KIT. It was a fantastic lecture and the prof was very good, but the scriptum was 600 pages long just for a few ECTS. I always wondered whether this project has industrial use somewhere or not.

throwawayjava 7y ago
The timsort bug: http://www.envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ http://www.envisage-project.eu/proving-android-java-and-pyth... Most software that's correctness critical is not written in Java. But I could see KeY-verified voting machines as at least better than the status quo (as long as you take it as an assumption that for whatever reason we absolutely need voting machines).
- wrs 7y ago
  But alas: > The reaction of the Java developer community to our report is somewhat disappointing: instead of using our fixed (and verified!) version of mergeCollapse(), they opted to increase the allocated runLen “sufficiently”. As we showed, this is not necessary. In consequence, whoever uses java.utils.Collection.sort() is forced to over allocate space.
nickpsecurity 7y ago
One I found on the website: https://www.key-project.org/2018/02/13/keys-sed-successfully-applied-in-an-industrial-setting/ https://www.key-project.org/2018/02/13/keys-sed-successfully... In an interesting coincidence, Hillel Wayne just did a write-up on applying Alloy to a similar scenario: https://www.hillelwayne.com/post/formally-modeling-migrations/ https://www.hillelwayne.com/post/formally-modeling-migration...