2020-11-16
History-based specification and verification of Java Collections in KeY
Publication
Publication
Presented at the
International Conference on Integrated Formal Methods (November 2020), Lugano, Switzerland
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).
| Additional Metadata | |
|---|---|
| , , | |
| doi.org/10.1007/978-3-030-63461-2_11 | |
| Lecture Notes in Computer Science | |
| International Conference on Integrated Formal Methods | |
| Organisation | Computer Security |
|
Hiep, H.-D., Bian, J., de Boer, F., & de Gouw, S. (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 |
|
