Verifying OpenJDK's LinkedList using KeY

Hans-Dieter A. Hiep*, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko C. J. D. van Eekelen, Stijn de Gouw

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

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.
Original languageEnglish
Title of host publicationTACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software
EditorsArmin Biere, David Parker
Place of PublicationCham
PublisherSpringer
Pages217-234
Number of pages18
ISBN (Electronic)978-3-030-45237-7
ISBN (Print)978-3-030-45236-0
DOIs
Publication statusPublished - 17 Apr 2020
Event(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020
Conference number: 26
https://etaps.org/2020/tacas
https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Publication series

SeriesLecture Notes in Computer Science
Volume12079
ISSN0302-9743
SeriesTheoretical Computer Science and General Issues (LNCS subseries)
Volume12079

Conference

Conference(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated titleTACAS 2020
Country/TerritoryIreland
CityDublin
Period25/04/2030/04/20
Internet address

Fingerprint

Dive into the research topics of 'Verifying OpenJDK's LinkedList using KeY'. Together they form a unique fingerprint.

Cite this