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.

, , , , ,
Achmea, Apeldoorn, The Netherlands
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