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

The work

TitleExperience Report on Formally Verifying Parts of OpenJDK's API with KeY
AuthorsAlexander Knüppel; Thomas Thüm; Carsten Pardylla; Ina Schaefer
Typearticle
Year2018
Citekeyknuppel2018experience

Where it appeared

Published inFormal Integrated Development Environment 2018 (F-IDE 2018)
PublisherOpen Publishing Association
SeriesElectronic Proceedings in Theoretical Computer Science
Volume284
Pages53--70

Identifiers

DOI10.4204/eptcs.284.5
OpenAlexW2950533071

Access

Landing pagehttps://doi.org/10.4204/eptcs.284.5
Free full texthttps://arxiv.org/pdf/1811.10818

Abstract

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.

Copy held

KindPDF, 241.3 kB
Retrieved2026-08-08
Heldlocal, for personal reference
Where it came fromhttps://doi.org/10.4204/eptcs.284.5

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Recordreviewed by a person
Approved2026-08-17
In: Do formal methods pay off? topic Electronic Proceedings in Theoretical Computer Science series Verifying real Java topic

Cite it as

@article{knuppel2018experience,
  title = {Experience Report on Formally Verifying Parts of OpenJDK's API with KeY},
  author = {Alexander Knüppel and Thomas Thüm and Carsten Pardylla and Ina Schaefer},
  year = {2018},
  journal = {Formal Integrated Development Environment 2018 (F-IDE 2018)},
  volume = {284},
  pages = {53--70},
  publisher = {Open Publishing Association},
  series = {Electronic Proceedings in Theoretical Computer Science},
  doi = {10.4204/eptcs.284.5},
  url = {https://arxiv.org/pdf/1811.10818},
}

This record lives at https://refs.drheap.org/knuppel2018experience/ and will keep doing so.