Integrating ADTs in KeY and their application to history-based reasoning about collection

DOI10.1007/s10703-023-00426-xOpenAlexW4381588017MaRDI QIDQ6185826

Frank S. de Boer, Stijn De Gouw, Jinting Bian, Hans-Dieter A. Hiep

Publication date: 8 January 2024

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-023-00426-x

zbMATH Keywords

formal verificationIsabelle/HOLabstract data typesprogram correctnessJMLKeYJava collection framework

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Foundations of algebraic specification and formal software development.
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving JDK's dual pivot quicksort correct
• Formal specification and verification of JDK's identity hash map implementation
• Proof pearl: The KeY to correct and stable sorting
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Dafny: An Automatic Program Verifier for Functional Correctness
• Hoare logic for Java in Isabelle/HOL
• Programming Languages and Systems
• Why3 — Where Programs Meet Provers
• Verification of Equivalent-Results Methods
• A case study in class library verification: Java's vector class

This page was built for publication: Integrating ADTs in KeY and their application to history-based reasoning about collection