Refinement to imperative HOL

DOI10.1007/S10817-017-9437-1zbMATH Open1465.68291OpenAlexW2762980364MaRDI QIDQ1739909FDOQ1739909

Authors 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

separation logicIsabelle/HOLrefinement calculusstepwise refinementimperative HOL

Mathematics Subject Classification ID

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

Recommendations

• Refinement to Imperative/HOL
• Imperative Functional Programming with Isabelle/HOL
• Automatic Data Refinement
• Efficient verification of imperative programs using auto2
• Applying data refinement for monadic programs to Hopcroft's algorithm

Cites work

• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• A theory of timed automata
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Automatic Data Refinement
• Characteristic formulae for the verification of imperative programs
• Fiat: deductive synthesis of abstract data types in a proof assistant
• Formalizing the Edmonds-Karp algorithm
• Imperative Functional Programming with Isabelle/HOL
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Mechanised Separation Algebra
• Partial and nested recursive function definitions in higher-order logic
• Permission accounting in separation logic
• Program development by stepwise refinement
• Refinement Calculus
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Ynot: dependent types for imperative programs

Cited in

(15)

• Imperative Functional Programming with Isabelle/HOL
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Refinement to Imperative/HOL
• From LCF to Isabelle/HOL
• A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
• Combining higher-order logic with set theory formalizations
• Data refinement in Isabelle/HOL
• Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
• A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
• A formally verified, optimized monitor for metric first-order dynamic logic
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• Trustworthy Graph Algorithms (Invited Talk)

Describes a project that uses

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

This page was built for publication: Refinement to imperative HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1739909)