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