Refinement to imperative HOL

DOI10.1007/s10817-017-9437-1zbMath1465.68291OpenAlexW2762980364MaRDI QIDQ1739909

Peter Lammich

Publication date: 29 April 2019

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

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/refinement-to-imperative-hol(3de7ca0b-1d46-4597-8f1b-378239c2c10d).html

zbMATH Keywords

stepwise refinementrefinement calculusseparation logicIsabelle/HOLimperative HOL

Mathematics Subject Classification ID

Data structures (68P05) General topics in the theory of algorithms (68W01) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation, A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL, Combining higher-order logic with set theory formalizations, Unnamed Item, For a few dollars more. Verified fine-grained algorithm analysis down to LLVM, From LCF to Isabelle/HOL, Trustworthy Graph Algorithms (Invited Talk), Integration of formal proof into unified assurance cases with Isabelle/SACM, A formally verified, optimized monitor for metric first-order dynamic logic

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• BEEM
• Ynot
• Autoref
• MLton
• Fiat
• Edmonds-Karp
• Separation Logic
• Dijkstra Shortest Path
• Refinement Monadic
• Collections
• Archive Formal Proofs
• CAVA LTL Modelchecker
• Gabow SCC
• Imperative Refinement

Cites Work

• Unnamed Item
• Partial and nested recursive function definitions in higher-order logic
• A theory of timed automata
• Fiat
• Formalizing the Edmonds-Karp Algorithm
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Mechanised Separation Algebra
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• Imperative Functional Programming with Isabelle/HOL
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Refinement Calculus
• Characteristic formulae for the verification of imperative programs
• Ynot
• Permission accounting in separation logic
• Automatic Data Refinement
• Program development by stepwise refinement
• Tools and Algorithms for the Construction and Analysis of Systems