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

The work

AuthorsAlexander Knüppel; Thomas Thüm; Carsten Pardylla; Ina Schaefer
Editors
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

arXiv1811.10818 from its oa_pdf_url
DOI10.4204/eptcs.284.5
OpenAlexW2950533071

Access

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

Related

Distinct frombatz2022foundations
Distinct frombian2021integrating
Distinct fromboer2022footprint
Distinct fromklein2018formally

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.

A copy is held

pdf, 235.6 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via openalex
Added2026-08-04 00:00 UTC
Approved bya person 2026-08-17 14:03 UTC

Filed under

do-formal-methods-pay eptcs verifying-real-java

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)},
  publisher    = {Open Publishing Association},
  series       = {Electronic Proceedings in Theoretical Computer Science},
  volume       = {284},
  pages        = {53--70},
  doi          = {10.4204/eptcs.284.5},
}

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