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
Recommendations
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)
Cites Work
- Ynot
- Automatic Data Refinement
- Fiat: deductive synthesis of abstract data types in a proof assistant
- Formalizing the Edmonds-Karp Algorithm
- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
- A theory of timed automata
- Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
- Refinement Calculus
- Characteristic formulae for the verification of imperative programs
- Program development by stepwise refinement
- Permission accounting in separation logic
- Partial and nested recursive function definitions in higher-order logic
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
- Tools and Algorithms for the Construction and Analysis of Systems
- Title not available (Why is that?)
- Imperative Functional Programming with Isabelle/HOL
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Mechanised Separation Algebra
Cited In (14)
- 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
- A formally verified, optimized monitor for metric first-order dynamic logic
- From LCF to Isabelle/HOL
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
- Title not available (Why is that?)
Uses Software
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)
