2020-04-25
Verifying OpenJDK's LinkedList using KeY
Publication
Publication
Presented at the
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (April 2020), Dublin, Ireland
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 | |
---|---|
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 | |
Organisation | 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
|