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.

Additional Metadata
Keywords Java standard library, Deductive verification, KeY, Java Modeling Language, Case study, Bug
Stakeholder Achmea, Apeldoorn, The Netherlands
Persistent URL dx.doi.org/10.1007/978-3-030-45237-7_13
Series Lecture Notes in Computer Science , Lecture Notes in Theoretical Computer Science and General Issues
Conference International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Citation
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