History-based specification and verification of Java Collections in KeY
In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java’s Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations including their parameters and return value, on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material).
|Formal verification, Interface specification, KeY|
|Lecture Notes in Computer Science|
|International Conference on Integrated Formal Methods|
Hiep, H.A, Bian, J, de Boer, F.S, & de Gouw, C.P.T. (2020). History-based specification and verification of Java Collections in KeY. In Integrated Formal Methods (pp. 199–217). doi:10.1007/978-3-030-63461-2_11