Integrating ADTs in KeY and their Application to History-based Reasoning: Proof Files
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep; Frank S. de Boer; Stijn de Gouw |
|---|---|
| Editors | |
| Type | misc |
| Year | 2021 |
| Citekey | bian2021integratingb |
Where it appeared
| Publisher | Zenodo |
|---|
Identifiers
| DOI | 10.5281/zenodo.4744268 |
|---|
Access
| Landing page | https://zenodo.org/record/4744268 |
|---|
Empty on purpose
| container, copy |
Related
| Distinct from | bian2021integrating |
|---|---|
| Distinct from | bian2022integrating |
Abstract
The project files for the article `Integrating ADTs in KeY and their Application to History-based reasoning.' The archive contains: The bundled version of KeY, key-2.8.0-exe.jar. The java source code of the project. Isabelle code (Collections. thy). The Isabelle version we use is Isabelle 2020. It can be download from the official website. Several user-defined lemmas that we need when we do the proof (addAll_rule.key) A number of proof files that can be loaded in KeY that verifies the contract for our case study. A document showing the proof settings in KeY. Compare to Version 1.0, this version updates the taclets which uses "find" and "replacewith". The taclet uses these two sentences correspond to a bi-implcation, since the term can appear on both sides of the sequent.
Cite it as
@misc{bian2021integratingb,
title = {Integrating ADTs in KeY and their Application to History-based Reasoning: Proof Files},
author = {Jinting Bian and Hans-Dieter A. Hiep and Frank S. de Boer and Stijn de Gouw},
year = {2021},
publisher = {Zenodo},
doi = {10.5281/zenodo.4744268},
}
This record lives at https://refs.drheap.org/bian2021integratingb/ and will keep doing so.