Integrating ADTs in KeY and Their Application to History-Based Reasoning

DOI10.1007/978-3-030-90870-6_14zbMath1521.68076MaRDI QIDQ6488468

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

Publication date: 21 April 2023

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

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

Cites Work

• 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
• 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
• 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