Integrating ADTs in KeY and Their Application to History-Based Reasoning

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

doi:10.1007/978-3-030-90870-6_14

Integrating ADTs in KeY and Their Application to History-Based Reasoning

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

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

Abstract

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.

Original language	English
Title of host publication	Formal Methods
Subtitle of host publication	24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings
Editors	Marieke Huisman, Corina Păsăreanu, Naijun Zhan
Place of Publication	Cham
Publisher	Springer
Pages	255-272
Number of pages	18
Edition	1
ISBN (Electronic)	978-3-030-90870-6
ISBN (Print)	978-3-030-90869-0
DOIs	https://doi.org/10.1007/978-3-030-90870-6_14
Publication status	Published - Nov 2021
Event	24th International Symposium on Formal Methods - Online, Beijing, China Duration: 20 Nov 2021 → 26 Nov 2021 https://link.springer.com/book/10.1007/978-3-030-90870-6

Publication series

Series	Lecture Notes in Computer Science
Volume	13047

Series	Programming and Software Engineering LNPSE
Volume	13047

Symposium

Symposium	24th International Symposium on Formal Methods
Abbreviated title	FM 2021
Country/Territory	China
City	Beijing
Period	20/11/21 → 26/11/21
Internet address	https://link.springer.com/book/10.1007/978-3-030-90870-6

Keywords

Abstract data type
Formal verification
Isabelle/HOL
Java Collection Framework
KeY
Program correctness

Access to Document

10.1007/978-3-030-90870-6_14

Cite this

Bian, Jinting ; Hiep, Hans-Dieter A. ; Boer, Frank S. de et al. / Integrating ADTs in KeY and Their Application to History-Based Reasoning. Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. editor / Marieke Huisman ; Corina Păsăreanu ; Naijun Zhan. 1. ed. Cham : Springer, 2021. pp. 255-272 (Lecture Notes in Computer Science, Vol. 13047). (Programming and Software Engineering LNPSE, Vol. 13047).

@inproceedings{9753cea83cb94b849d79ff97e67166f3,

title = "Integrating ADTs in KeY and Their Application to History-Based Reasoning",

abstract = "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{\textquoteright}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.",

keywords = "Abstract data type, Formal verification, Isabelle/HOL, Java Collection Framework, KeY, Program correctness",

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

year = "2021",

month = nov,

doi = "10.1007/978-3-030-90870-6_14",

language = "English",

isbn = "978-3-030-90869-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "255--272",

editor = "Marieke Huisman and Corina P{\u a}s{\u a}reanu and Naijun Zhan",

booktitle = "Formal Methods",

edition = "1",

note = "24th International Symposium on Formal Methods, FM 2021 ; Conference date: 20-11-2021 Through 26-11-2021",

url = "https://link.springer.com/book/10.1007/978-3-030-90870-6",

}

Bian, J, Hiep, H-DA, Boer, FSD & Gouw, SD 2021, Integrating ADTs in KeY and Their Application to History-Based Reasoning. in M Huisman, C Păsăreanu & N Zhan (eds), Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. 1 edn, Springer, Cham, Lecture Notes in Computer Science, vol. 13047, Programming and Software Engineering LNPSE, vol. 13047, pp. 255-272, 24th International Symposium on Formal Methods, Beijing, China, 20/11/21. https://doi.org/10.1007/978-3-030-90870-6_14

Integrating ADTs in KeY and Their Application to History-Based Reasoning. / Bian, Jinting; Hiep, Hans-Dieter A.; Boer, Frank S. de et al.
Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. ed. / Marieke Huisman; Corina Păsăreanu; Naijun Zhan. 1. ed. Cham: Springer, 2021. p. 255-272 (Lecture Notes in Computer Science, Vol. 13047). (Programming and Software Engineering LNPSE, Vol. 13047).

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

TY - GEN

T1 - Integrating ADTs in KeY and Their Application to History-Based Reasoning

AU - Bian, Jinting

AU - Hiep, Hans-Dieter A.

AU - Boer, Frank S. de

AU - Gouw, Stijn de

PY - 2021/11

Y1 - 2021/11

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

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

KW - Abstract data type

KW - Formal verification

KW - Isabelle/HOL

KW - Java Collection Framework

KW - KeY

KW - Program correctness

U2 - 10.1007/978-3-030-90870-6_14

DO - 10.1007/978-3-030-90870-6_14

M3 - Conference Article in proceeding

SN - 978-3-030-90869-0

T3 - Lecture Notes in Computer Science

SP - 255

EP - 272

BT - Formal Methods

A2 - Huisman, Marieke

A2 - Păsăreanu, Corina

A2 - Zhan, Naijun

PB - Springer

CY - Cham

T2 - 24th International Symposium on Formal Methods

Y2 - 20 November 2021 through 26 November 2021

ER -

Bian J, Hiep HDA, Boer FSD, Gouw SD. Integrating ADTs in KeY and Their Application to History-Based Reasoning. In Huisman M, Păsăreanu C, Zhan N, editors, Formal Methods: 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings. 1 ed. Cham: Springer. 2021. p. 255-272. (Lecture Notes in Computer Science, Vol. 13047). (Programming and Software Engineering LNPSE, Vol. 13047). doi: 10.1007/978-3-030-90870-6_14

Integrating ADTs in KeY and Their Application to History-Based Reasoning

Abstract

Publication series

Symposium

Keywords

Access to Document

Fingerprint

Cite this