Verifying OpenJDK’s LinkedList using KeY

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.

Detalles Bibliográficos
Autores principales: Hiep, Hans-Dieter A., Maathuis, Olaf, Bian, Jinting, de Boer, Frank S., van Eekelen, Marko, de Gouw, Stijn
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480693/
http://dx.doi.org/10.1007/978-3-030-45237-7_13
_version_ 1783580460733956096
author Hiep, Hans-Dieter A.
Maathuis, Olaf
Bian, Jinting
de Boer, Frank S.
van Eekelen, Marko
de Gouw, Stijn
author_facet Hiep, Hans-Dieter A.
Maathuis, Olaf
Bian, Jinting
de Boer, Frank S.
van Eekelen, Marko
de Gouw, Stijn
author_sort Hiep, Hans-Dieter A.
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7480693
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74806932020-09-10 Verifying OpenJDK’s LinkedList using KeY Hiep, Hans-Dieter A. Maathuis, Olaf Bian, Jinting de Boer, Frank S. van Eekelen, Marko de Gouw, Stijn Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2020-03-13 /pmc/articles/PMC7480693/ http://dx.doi.org/10.1007/978-3-030-45237-7_13 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Hiep, Hans-Dieter A.
Maathuis, Olaf
Bian, Jinting
de Boer, Frank S.
van Eekelen, Marko
de Gouw, Stijn
Verifying OpenJDK’s LinkedList using KeY
title Verifying OpenJDK’s LinkedList using KeY
title_full Verifying OpenJDK’s LinkedList using KeY
title_fullStr Verifying OpenJDK’s LinkedList using KeY
title_full_unstemmed Verifying OpenJDK’s LinkedList using KeY
title_short Verifying OpenJDK’s LinkedList using KeY
title_sort verifying openjdk’s linkedlist using key
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480693/
http://dx.doi.org/10.1007/978-3-030-45237-7_13
work_keys_str_mv AT hiephansdietera verifyingopenjdkslinkedlistusingkey
AT maathuisolaf verifyingopenjdkslinkedlistusingkey
AT bianjinting verifyingopenjdkslinkedlistusingkey
AT deboerfranks verifyingopenjdkslinkedlistusingkey
AT vaneekelenmarko verifyingopenjdkslinkedlistusingkey
AT degouwstijn verifyingopenjdkslinkedlistusingkey

Ejemplares similares