2020-07-23
History-based specification and verification of Java collections in KeY (keynote)
Publication
Publication
Presented at the
ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020
Software libraries, such as the Java Collection Framework, are used by many applications: Thus their correctness is of utmost importance. The state-of-the-art KeY system can be used to formally reason about program correctness of Java programs. Recently, KeY has been used to show major flaws in the Java Collection Framework. However, some methods are challenging for verification, namely those involving parameters of interface type. This lecture discussed a new history-based specification method for reasoning about the correctness of clients and arbitrary implementations of interfaces, and the Collection interface in particular.
| Additional Metadata | |
|---|---|
| , , | |
| doi.org/10.1145/3427761.3432349 | |
| ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
de Boer, F., & Hiep, H.-D. (2020). History-based specification and verification of Java collections in KeY (keynote). In FTfJP 2020 - Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs, FTfJP 2020, co-located with ECOOP 2020/SPLASH 2020 (pp. 2–3). doi:10.1145/3427761.3432349 |
|
