Integrating ADTs in KeY and their application to history-based reasoning about collection

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

doi:10.1007/s10703-023-00426-x

Integrating ADTs in KeY and their application to history-based reasoning about collection

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

^*Corresponding author for this work

Research output: Contribution to journal › Article › 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 represent Isabelle theorems as 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. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

Original language	English
Pages (from-to)	63-89
Journal	Formal Methods in System Design
Volume	61
Issue number	1
DOIs	https://doi.org/10.1007/s10703-023-00426-x
Publication status	Published - 9 May 2023

Keywords

Abstract data types
Formal verification
Isabelle/HOL
Java collection framework
JML
KeY
Program correctness

Access to Document

10.1007/s10703-023-00426-xLicence: CC BY

Cite this

@article{9b7d229ea5244e89935e1426454843ae,

title = "Integrating ADTs in KeY and their application to history-based reasoning about collection",

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 represent Isabelle theorems as 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. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).",

keywords = "Abstract data types, Formal verification, Isabelle/HOL, Java collection framework, JML, KeY, Program correctness",

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

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s).",

year = "2023",

month = may,

day = "9",

doi = "10.1007/s10703-023-00426-x",

language = "English",

volume = "61",

pages = "63--89",

journal = "Formal Methods in System Design",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "1",

}

TY - JOUR

T1 - Integrating ADTs in KeY and their application to history-based reasoning about collection

AU - Bian, Jinting

AU - Hiep, Hans Dieter A.

AU - de Boer, Frank S.

AU - de Gouw, Stijn

PY - 2023/5/9

Y1 - 2023/5/9

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 represent Isabelle theorems as 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. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

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 represent Isabelle theorems as 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. Open Science. Includes video material (Bian and Hiep in FigShare, 2021. https://doi.org/10.6084/m9.figshare.c.5413263) and a source code artifact (Bian et al. in Zenodo, 2022. https://doi.org/10.5281/zenodo.7079126).

KW - Abstract data types

KW - Formal verification

KW - Isabelle/HOL

KW - Java collection framework

KW - JML

KW - KeY

KW - Program correctness

UR - http://www.scopus.com/inward/record.url?scp=85158987772&partnerID=8YFLogxK

U2 - 10.1007/s10703-023-00426-x

DO - 10.1007/s10703-023-00426-x

M3 - Article

AN - SCOPUS:85158987772

SN - 0925-9856

VL - 61

SP - 63

EP - 89

JO - Formal Methods in System Design

JF - Formal Methods in System Design

IS - 1

ER -

Integrating ADTs in KeY and their application to history-based reasoning about collection

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this