Experience Report on Formally Verifying Parts of OpenJDK's API with KeY

Alexander Knüppel, Thomas Thüm, Carsten Pardylla +1

Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-term perspective is, h…