Hacker News new | past | comments | ask | show | jobs | submit login
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY (arxiv.org)
31 points by snaky 3 months ago | hide | past | web | favorite | 2 comments

Huh, interesting that they picked OpenJDK 6 for this work. Any clue why?

I suspect that it is because Java 6 is the oldest (and thus smallest/simplest) version of Java that supports their tooling. Java 6 introduced annotations which makes writing third party tooling a lot easier plus Java 7 changed the sort algorithm. This particular update which used Timsort actually had some subtle issues which were only found through formal verification [1]. Not sure if there were other changes to collections internally/externally though.

[1]: http://www.envisage-project.eu/proving-android-java-and-pyth...

Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact