FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Experience Report on Formally Verifying Parts of OpenJDK's API with KeY

Authors: Alexander Knüppel, Carsten Pardylla, Thomas Thüm and Ina Schaefer

Paper Information

Title:Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
Authors:Alexander Knüppel, Carsten Pardylla, Thomas Thüm and Ina Schaefer
Proceedings:F-IDE F-IDE-18 Proceedings
Editors: Paolo Masci, Rosemary Monahan and Virgile Prevosto
Keywords:deductive verification, design by contract, formal methods, theorem proving, KeY, OpenJDK
Abstract:

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.

Pages:18
Talk:Jul 14 15:00 (Session 98B: Experience in analyzing large programs)
Paper: