Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Bian, J., Hiep, H.A.: Verifying OpenJDK’s LinkedList using KeY: Video (2019). https://doi.org/10.6084/m9.figshare.10033094.v2
Hiep, H.A., Maathuis, O., Bian, J., de Boer, F.S., van Eekelen, M., de Gouw, S.: Verifying OpenJDK’s LinkedList using KeY: Proof Files (2019). https://doi.org/10.5281/zenodo.3517081
Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification: The KeY Book, LNCS, vol. 10001. Springer (2016). https://doi.org/10.1007/978-3-319-49812-6
Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification–specification is the new bottleneck. In: SSV 2012: Systems Software Verification. EPTCS, vol. 102, pp. 18–32. OPA (2012). https://doi.org/10.4204/EPTCS.102.4
Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: Verification of parallel and concurrent software. In: iFM 2017: Integrated Formal Methods. LNCS, vol. 10510, pp. 102–110. Springer (2017). https://doi.org/10.1007/978-3-319-66845-1_7
Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: F-IDE 2014: Workshop on Formal Integrated Development Environment. EPTCS, vol. 149, pp. 79–92. OPA (2014). https://doi.org/10.4204/EPTCS.149.8
de Gouw, S., de Boer, F.S., Bubel, R., Hähnle, R., Rot, J., Steinhöfel, D.: Verifying OpenJDK’s Sort Method for Generic Collections. Journal of Automated Reasoning 62(1), 93–126 (2017). https://doi.org/10.1007/s10817-017-9426-4
de Gouw, S., de Boer, F.S., Rot, J.: Proof Pearl: The KeY to Correct and Stable Sorting. Journal of Automated Reasoning 53(2), 129–139 (2014). https://doi.org/10.1007/s10817-013-9300-y
de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s java.utils.Collection.sort() is broken: The good, the bad and the worst case. In: CAV 2015: Computer Aided Verification. LNCS, vol. 9206, pp. 273–289. Springer (2015). https://doi.org/10.1007/978-3-319-21690-4_16
Huisman, M., Ahrendt, W., Bruns, D., Hentschel, M.: Formal specification with JML. Tech. rep., Karlsruher Institut für Technologie (KIT) (2014). https://doi.org/10.5445/IR/1000041881
Ieu Eauvidoum, disk noise: Twenty years of escaping the Java sandbox. Phrack Magazine (September 2018), http://www.phrack.org/papers/escaping_the_java_sandbox.html
Klebanov, V., Müller, P., et al.: The 1st verified software competition: Experience report. In: FM 2011: Formal Methods. LNCS, vol. 6664, pp. 154–168. Springer (2011). https://doi.org/10.1007/978-3-642-21437-0_14
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM TOPLAS 28(4), 619–695 (2006). https://doi.org/10.1145/1146809.1146811
Knüppel, A., Thüm, T., Pardylla, C., Schaefer, I.: Experience report on formally verifying parts of OpenJDK’s API with KeY. In: F-IDE 2018: Formal Integrated Development Environment. EPTCS, vol. 284, pp. 53–70. OPA (2018). https://doi.org/10.4204/EPTCS.284.5
Knuth, D.E.: The art of computer programming, vol. 1. Addison-Wesley, 3rd edn. (1997) ISBN: 978-0-201-89683-4
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, SECS, vol. 523, pp. 175–188. Springer (1999). https://doi.org/10.1007/978-1-4615-5229-1_12
Nipkow, T., von Oheimb, D.: Javalight is type-safe–definitely. In: POPL 1998: Principles of Programming Languages. pp. 161–170. ACM (1998). https://doi.org/10.1145/268946.268960
Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: FM 2015: Formal Methods. LNCS, vol. 9109, pp. 414–434. Springer (2015). https://doi.org/10.1007/978-3-319-19249-9_26
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Hiep, HD.A., Maathuis, O., Bian, J., de Boer, F.S., van Eekelen, M., de Gouw, S. (2020). Verifying OpenJDK’s LinkedList using KeY. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)