Automatic refinement to efficient data structures: a comparison of two approaches

DOI10.1007/s10817-018-9461-9zbMath1459.68228OpenAlexW2790446557WikidataQ130078532 ScholiaQ130078532MaRDI QIDQ2417948

Andreas Lochbihler, Peter Lammich

Publication date: 31 May 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-9461-9

zbMATH Keywords

data refinementcode generationalgorithm verification

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Quotients of Bounded Natural Functors ⋮ Unnamed Item

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• CeTA
• Locales
• Autoref
• Transfer
• Lifting
• Fiat
• Dijkstra Shortest Path
• CAVA Automata Library
• CAVA
• Presburger Automata
• Archive Formal Proofs
• CAVA LTL Modelchecker
• Tree Automata
• Gabow SCC
• Light-weight Containers
• LTL_to_GBA
• Real_Impl

Cites Work

• Unnamed Item
• Reachability, confluence, and termination analysis with state-compatible automata
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formal verification of an executable LTL model checker with partial order reduction
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A formal proof in Coq of Lasalle's invariance principle
• Locales: a module system for mathematical theories
• Proof of correctness of data representations
• A formally verified compiler back-end
• Fiat
• Automatic Functional Correctness Proofs for Functional Search Trees
• Truly Modular (Co)datatypes for Isabelle/HOL
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Refinements for Free!
• Refinement to Imperative/HOL
• Deriving Comparators and Show Functions in Isabelle/HOL
• Animating the Formalised Semantics of a Java-Like Language
• Formalizing the Logic-Automaton Connection
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Certification of Termination Proofs Using CeTA
• First-Class Type Classes
• Code Generation via Higher-Order Rewrite Systems
• Refinement Calculus
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• Theorem Proving in Higher Order Logics
• Program development by stepwise refinement
• The Isabelle Collections Framework