Verifying OpenJDK’s LinkedList using KeY (extended paper)

International Journal on Software Tools for Technology Transfer, vol. 24, pp. 783–802

Abstract

Abstract As a particular case study of the formal verification of state-of-the-art, real software, we discuss the specification and verification of a corrected version of the implementation of a linked list as provided by the Java Collection Framework.

Authors 5

1. Hans-Dieter A. Hiep corresponding Aachen Leiden Institute of Advanced Computer Science

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   Centrum Wiskunde & Informatica (CWI), Amsterdam, the Netherlands

   Leiden Institute of Advanced Computer Science (LIACS), Leiden, the Netherlands

2. Olaf Maathuis corresponding

   Achmea (Netherlands)

   Affiliation as printed

   Achmea, Zeist, the Netherlands

3. Jinting Bian corresponding Aachen Leiden Institute of Advanced Computer Science

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   Centrum Wiskunde & Informatica (CWI), Amsterdam, the Netherlands

   Leiden Institute of Advanced Computer Science (LIACS), Leiden, the Netherlands

4. Frank S. de Boer corresponding Aachen Leiden Institute of Advanced Computer Science

   Leiden University · Centrum Wiskunde & Informatica

   Affiliation as printed

   Centrum Wiskunde & Informatica (CWI), Amsterdam, the Netherlands

   Leiden Institute of Advanced Computer Science (LIACS), Leiden, the Netherlands

5. Stijn de Gouw corresponding

   Centrum Wiskunde & Informatica · Open University of the Netherlands

   Affiliation as printed

   Centrum Wiskunde & Informatica (CWI), Amsterdam, the Netherlands

   Open University (OU), Heerlen, the Netherlands