History-Based Specification and Verification of Java Collections in KeY

Hans-Dieter A. Hiep; Jinting Bian; Frank S. de Boer; Stijn de Gouw

doi:10.1007/978-3-030-63461-2_11

History-Based Specification and Verification of Java Collections in KeY

Hans-Dieter A. Hiep, Jinting Bian, Frank S. de Boer, Stijn de Gouw

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

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).

Original language	English
Title of host publication	Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings
Subtitle of host publication	16th International Conference, IFM 2020
Editors	Brijesh Dongol, Elena Troubitsyna
Place of Publication	Lugano, Switzerland
Publisher	Springer
Pages	199-217
Number of pages	19
ISBN (Electronic)	9783030634612
ISBN (Print)	9783030634605
DOIs	https://doi.org/10.1007/978-3-030-63461-2_11
Publication status	Published - 13 Nov 2020
Event	16th international conference, Integrated Formal Methods 2020 - Online, Lugano, Switzerland Duration: 16 Nov 2020 → 20 Nov 2020 Conference number: 16 https://ifm20.si.usi.ch/

Publication series

Series	Lecture Notes in Computer Science
ISSN	0302-9743

Conference

Conference	16th international conference, Integrated Formal Methods 2020
Abbreviated title	IFM 2020
Country/Territory	Switzerland
City	Lugano
Period	16/11/20 → 20/11/20
Internet address	https://ifm20.si.usi.ch/

Keywords

Formal verification
Interface specification
KeY

Access to Document

10.1007/978-3-030-63461-2_11

Cite this

Hiep, Hans-Dieter A. ; Bian, Jinting ; Boer, Frank S. de et al. / History-Based Specification and Verification of Java Collections in KeY. Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings: 16th International Conference, IFM 2020. editor / Brijesh Dongol ; Elena Troubitsyna. Lugano, Switzerland : Springer, 2020. pp. 199-217 (Lecture Notes in Computer Science).

@inproceedings{effb850848904919bb499d1c35b10251,

title = "History-Based Specification and Verification of Java Collections in KeY",

abstract = "In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java{\textquoteright}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).",

keywords = "Formal verification, Interface specification, KeY",

author = "Hiep, {Hans-Dieter A.} and Jinting Bian and Boer, {Frank S. de} and Gouw, {Stijn de}",

year = "2020",

month = nov,

day = "13",

doi = "10.1007/978-3-030-63461-2_11",

language = "English",

isbn = "9783030634605",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "199--217",

editor = "Brijesh Dongol and Elena Troubitsyna",

booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings",

note = "16th international conference, Integrated Formal Methods 2020, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",

url = "https://ifm20.si.usi.ch/",

}

Hiep, H-DA, Bian, J, Boer, FSD & Gouw, SD 2020, History-Based Specification and Verification of Java Collections in KeY. in B Dongol & E Troubitsyna (eds), Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings: 16th International Conference, IFM 2020. Springer, Lugano, Switzerland, Lecture Notes in Computer Science, pp. 199-217, 16th international conference, Integrated Formal Methods 2020, Lugano, Switzerland, 16/11/20. https://doi.org/10.1007/978-3-030-63461-2_11

History-Based Specification and Verification of Java Collections in KeY. / Hiep, Hans-Dieter A.; Bian, Jinting; Boer, Frank S. de et al.
Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings: 16th International Conference, IFM 2020. ed. / Brijesh Dongol; Elena Troubitsyna. Lugano, Switzerland: Springer, 2020. p. 199-217 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - History-Based Specification and Verification of Java Collections in KeY

AU - Hiep, Hans-Dieter A.

AU - Bian, Jinting

AU - Boer, Frank S. de

AU - Gouw, Stijn de

N1 - Conference code: 16

PY - 2020/11/13

Y1 - 2020/11/13

N2 - 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).

AB - 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).

KW - Formal verification

KW - Interface specification

KW - KeY

U2 - 10.1007/978-3-030-63461-2_11

DO - 10.1007/978-3-030-63461-2_11

M3 - Conference Article in proceeding

SN - 9783030634605

T3 - Lecture Notes in Computer Science

SP - 199

EP - 217

BT - Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings

A2 - Dongol, Brijesh

A2 - Troubitsyna, Elena

PB - Springer

CY - Lugano, Switzerland

T2 - 16th international conference, Integrated Formal Methods 2020

Y2 - 16 November 2020 through 20 November 2020

ER -

Hiep HDA, Bian J, Boer FSD, Gouw SD. History-Based Specification and Verification of Java Collections in KeY. In Dongol B, Troubitsyna E, editors, Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings: 16th International Conference, IFM 2020. Lugano, Switzerland: Springer. 2020. p. 199-217. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-63461-2_11

History-Based Specification and Verification of Java Collections in KeY

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this