Refinement to imperative HOL

DOI10.1007/S10817-017-9437-1MaRDI QIDQ1739909zbMATH OpenOpenAlexFDO

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

(19)

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

Describes a project that uses

Uses Software

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

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)