figshare
Browse

History-based Specification and Verification of Java Collections in KeY: Video Material

Version 3 2020-07-03, 08:58
Version 2 2020-06-18, 14:02
Version 1 2020-06-11, 10:54
Posted on 2020-07-03 - 08:58 authored by Hans-Dieter A. Hiep
The video collection contains a number of videos that demonstrate the construction of proofs for showing the history-based verification of clients and interface implementations. It accompanies a paper with the following abstract:

"In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java’s Collection interface. We introduce a new specification method (in KeY) using histories, that records method invocations and their parameters on an interface. We outline the challenges of proving clients correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY."

CITE THIS COLLECTION

DataCite
3 Biotech
3D Printing in Medicine
3D Research
3D-Printed Materials and Systems
4OR
AAPG Bulletin
AAPS Open
AAPS PharmSciTech
Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg
ABI Technik (German)
Academic Medicine
Academic Pediatrics
Academic Psychiatry
Academic Questions
Academy of Management Discoveries
Academy of Management Journal
Academy of Management Learning and Education
Academy of Management Perspectives
Academy of Management Proceedings
Academy of Management Review
or
Select your citation style and then place your mouse over the citation text to select it.

SHARE

email
need help?