• Integrating ADTs in KeY and th...

Treffer: Integrating ADTs in KeY and their Application to History-based Reasoning: Proof Files

Title:
Integrating ADTs in KeY and their Application to History-based Reasoning: Proof Files
Authors:
Jinting Bian, orcid:0000-0001-9677-, Hans-Dieter A. Hiep, Frank S. de Boer, Stijn de Gouw
Publisher Information:
Zenodo
Publication Year:
2021
Collection:
Zenodo
Subject Terms:
Formal methods, abstract data type, program correctness, Java Collection Framework, KeY
Document Type:
E-Ressource software
Language:
unknown
Relation:
https://zenodo.org/records/4744269; oai:zenodo.org:4744269; https://doi.org/10.5281/zenodo.4744269
DOI:
10.5281/zenodo.4744269
Availability:
https://doi.org/10.5281/zenodo.4744269
https://zenodo.org/records/4744269
Rights:
Creative Commons Attribution 4.0 International ; cc-by-4.0 ; https://creativecommons.org/licenses/by/4.0/legalcode
Accession Number:
edsbas.CF1EEE65
Database:
BASE

Weitere Informationen

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.