We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs
< prev | next >
new | recent | 1911

Change to browse by:

cs.LO
cs.SE

References & Citations

DBLP - CS Bibliography

listing | bibtex

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Logic in Computer Science

Title: Verifying OpenJDK's LinkedList using KeY

Authors: Hans-Dieter A. Hiep, Olaf Maathuis, Jinting Bian, Frank S. de Boer, Marko van Eekelen, Stijn de Gouw
(Submitted on 11 Nov 2019)
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. Keywords: Java, standard library, deductive verification, KeY, Java Modeling Language, case study, bug
Comments: 16 pages, 9 pages appendix
Subjects: Logic in Computer Science (cs.LO); Software Engineering (cs.SE)
Cite as: arXiv:1911.04195 [cs.LO]
  (or arXiv:1911.04195v1 [cs.LO] for this version)

Submission history

From: Hans-Dieter A. Hiep [view email]
[v1] Mon, 11 Nov 2019 11:39:54 GMT (538kb)
Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

Link back to: arXiv, form interface, contact.