The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Integrating ADTs in KeY and their Application to History-based Reasoning : Video Material
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
This is the collection of video material that used in "Integrating ADTs in KeY and their Application to History-based Reasoning". It contains screen recordings of interactive proof sessions with the KeY theorem prover. Each video displays how to create a proof for case study. The method contracts are expressed in the Java Modeling Language (not shown in the video). 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.
@misc{bian2021integratingc,
title = {Integrating ADTs in KeY and their Application to History-based Reasoning : Video Material},
author = {Jinting Bian and Hans-Dieter A. Hiep},
year = {2021},
journal = {Data Archiving and Networked Services (DANS)},
publisher = {Royal Netherlands Academy of Arts and Sciences},
doi = {10.6084/m9.figshare.c.5413263},
}