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 | |
|---|---|
| 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
|
