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 proceedingConference article in proceedingAcademicpeer-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 languageEnglish
Title of host publicationFormal Methods
Subtitle of host publication24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings
EditorsMarieke Huisman, Corina S. Pasareanu, Naijun Zhan
Place of PublicationCham
PublisherSpringer
Pages255-272
Number of pages18
Edition1
ISBN (Electronic)978-3-030-90870-6
ISBN (Print)978-3-030-90869-0
DOIs
Publication statusPublished - Nov 2021
Event24th International Symposium on Formal Methods - Online, Beijing, China
Duration: 20 Nov 202126 Nov 2021
https://link.springer.com/book/10.1007/978-3-030-90870-6

Publication series

SeriesLecture Notes in Computer Science
Volume13047
SeriesProgramming and Software Engineering LNPSE
Volume13047

Symposium

Symposium24th International Symposium on Formal Methods
Abbreviated titleFM 2021
Country/TerritoryChina
CityBeijing
Period20/11/2126/11/21
Internet address

Fingerprint

Dive into the research topics of 'Integrating ADTs in KeY and Their Application to History-Based Reasoning'. Together they form a unique fingerprint.

Cite this