Refinement to Imperative/HOL

DOI10.1007/978-3-319-22102-1_17MaRDI QIDQ2945637zbMATH OpenOpenAlexFDO

Authors Peter Lammich

Publication date 14 September 2015

Published in Interactive Theorem Proving (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

Mathematics Subject Classification ID

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

Recommendations

• Refinement to imperative HOL
• scientific article; zbMATH DE number 1368953
• Refinement of intentions
• Implicational rewriting tactics in HOL
• Refinement concepts formalised in higher order logic
• Fine-tuning natural language imperatives
• Understanding, Explaining, and Deriving Refinement
• scientific article; zbMATH DE number 2148397
• scientific article; zbMATH DE number 1086636

Cites work

• Applying data refinement for monadic programs to Hopcroft's algorithm
• Automatic Data Refinement
• Characteristic formulae for the verification of imperative programs
• Compositional shape analysis by means of bi-abduction
• Finger trees: a simple general-purpose data structure
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Mechanised Separation Algebra
• Permission accounting in separation logic
• The Isabelle collections framework
• 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

(28)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Refinement to imperative HOL
• Verified memoization and dynamic programming
• Verifying asymptotic time complexity of imperative programs in Isabelle
• Proof-producing synthesis of CakeML from monadic HOL functions
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Automatic refinement to efficient data structures: a comparison of two approaches
• Rule-based static analysis of network protocol implementations
• Formalizing the Edmonds-Karp algorithm
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Refinements for free!
• Verified characteristic formulae for CakeML
• Imperative Functional Programming with Isabelle/HOL
• Verified certification of reachability checking for timed automata
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• Efficient Verified Implementation of Introsort and Pdqsort
• Data refinement in Isabelle/HOL
• The Isabelle collections framework
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Efficient verified (UN)SAT certificate checking
• Gale-Shapley verified
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
• Formal verification of an executable LTL model checker with partial order reduction
• Fast and verified UNSAT certificate checking

Describes a project that uses

Uses Software

• Isabelle
• HOL
• BEEM
• MLton
• Dijkstra Shortest Path
• Separation Logic
• Isabelle/HOL

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 Q2945637)