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.

Java standard library, Deductive verification, KeY, Java Modeling Language, Case study, Bug
Achmea, Apeldoorn, The Netherlands
dx.doi.org/10.1007/978-3-030-45237-7_13
Lecture Notes in Computer Science , Lecture Notes in Theoretical Computer Science and General Issues
International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Computer Security

Hiep, H.A, Maathuis, O, Bian, J, de Boer, F.S, van Eekelen, M, & de Gouw, C.P.T. (2020). Verifying OpenJDK's LinkedList using KeY. In TACAS 2020: Tools and Algorithms for the Construction and Analysis of Systems (pp. 217–234). doi:10.1007/978-3-030-45237-7_13