2021-11-10
Integrating ADTs in KeY and their application to history-based reasoning
Publication
Publication
Presented at the
24th International Symposium on Formal Methods, FM 2021 (November 2021), Beijing, China
We discuss integrating abstract data types (ADTs) in the KeY theorem prover by a new approach to model data types using Isabelle/HOL as an interactive back-end, and translate Isabelle theorems to user-defined taclets in KeY. As a case study of this new approach, we reason about Java’s Collection interface using histories, and we prove the correctness of several clients that operate on multiple objects, thereby significantly improving the state-of-the-art of history-based reasoning.
| Additional Metadata | |
|---|---|
| , , , , , | |
| doi.org/10.1007/978-3-030-90870-6_14 | |
| Lecture Notes in Computer Science | |
| 24th International Symposium on Formal Methods, FM 2021 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
Bian, J., Hiep, H.-D., de Boer, F., & de Gouw, S. (2021). Integrating ADTs in KeY and their application to history-based reasoning. In Proceedings of the 24th International Symposium on Formal Methods, FM 2021 (pp. 255–272). doi:10.1007/978-3-030-90870-6_14 |
|
| See Also |
|---|
