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

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

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

Computer Science > Logic in Computer Science

Title: Verifying OpenJDK's LinkedList using KeY

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)

Link back to: arXiv, form interface, contact.