Integrating ADTs in KeY and their application to history-based reasoning about collection
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep; Frank S. de Boer; Stijn de Gouw |
|---|---|
| Editors | |
| Type | article |
| Year | 2022 |
| Citekey | bian2022integrating |
Where it appeared
| Published in | Formal Methods in System Design |
|---|---|
| Publisher | Springer Science and Business Media LLC |
| Volume | 61 |
| Issue | 1 |
| Pages | 63--89 |
Identifiers
| DOI | 10.1007/s10703-023-00426-x |
|---|---|
| OpenAlex | W4381588017 |
Access
| Landing page | https://doi.org/10.1007/s10703-023-00426-x |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/s10703-023-00426-x.pdf |
Related
| Distinct from | bian2021integrating |
|---|---|
| Distinct from | bian2021integratingb |
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 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 ).
Cite it as
@article{bian2022integrating,
title = {Integrating ADTs in KeY and their application to history-based reasoning about collection},
author = {Jinting Bian and Hans-Dieter A. Hiep and Frank S. de Boer and Stijn de Gouw},
year = {2022},
journal = {Formal Methods in System Design},
publisher = {Springer Science and Business Media LLC},
volume = {61},
number = {1},
pages = {63--89},
doi = {10.1007/s10703-023-00426-x},
}
This record lives at https://refs.drheap.org/bian2022integrating/ and will keep doing so.