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

• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• 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
• 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

(27)

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

Describes a project that uses

Uses Software

• Dijkstra Shortest Path
• Separation Logic
• MLton
• 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 Q2945637)