Integrating ADTs in KeY and their application to history-based reasoning about collection
From MaRDI portal
Recommendations
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- On keys and functional dependencies as first-class citizens in description logics
- On Keys and Functional Dependencies as First-Class Citizens in Description Logics
- Collecting Semantics under Predicate Abstraction in the K Framework
- scientific article; zbMATH DE number 2243355
- Automated reasoning about key sets
- “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics
- scientific article; zbMATH DE number 1304366
Cites work
- A case study in class library verification: Java's vector class
- Dafny: an automatic program verifier for functional correctness
- Formal specification and verification of JDK's identity hash map implementation
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Foundations of algebraic specification and formal software development.
- Hoare logic for Java in Isabelle/HOL
- scientific article; zbMATH DE number 2090026 (Why is no real title available?)
- scientific article; zbMATH DE number 7526287 (Why is no real title available?)
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- Isabelle/HOL. A proof assistant for higher-order logic
- Programming Languages and Systems
- Proof pearl: The KeY to correct and stable sorting
- Proving JDK's dual pivot quicksort correct
- Verification of Equivalent-Results Methods
- Why3 -- where programs meet provers
This page was built for publication: Integrating ADTs in KeY and their application to history-based reasoning about collection
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6185826)
