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

Alexander Knüppel
Thomas Thüm
Carsten Pardylla
Ina Schaefer

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, however, to develop verification tools aiding industrial software developers to find bugs or bottlenecks in software systems faster and more easily. The KeY project constitutes a framework for specifying and verifying software systems, aiming at making formal verification tools applicable for mainstream software development. To help the developers of KeY, its users, and the deductive verification community, we summarize our experiences with KeY 2.6.1 in specifying and verifying real-world Java code from a users perspective. To this end, we concentrate on parts of the Collections-API of OpenJDK 6, where an informal specification exists. While we describe how we bridged informal and formal specification, we also exhibit accompanied challenges that we encountered. Our experiences are that (a) in principle, deductive verification for API-like code bases is feasible, but requires high expertise, (b) developing formal specifications for existing code bases is still notoriously hard, and (c) the under-specification of certain language constructs in Java is challenging for tool builders. Our initial effort in specifying parts of OpenJDK 6 constitutes a stepping stone towards a case study for future research.

In Paolo Masci, Rosemary Monahan and Virgile Prevosto: Proceedings 4th Workshop on Formal Integrated Development Environment (F-IDE 2018), Oxford, England, 14 July 2018, Electronic Proceedings in Theoretical Computer Science 284, pp. 53–70.
Published: 27th November 2018.

ArXived at: https://dx.doi.org/10.4204/EPTCS.284.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org