Refinement to Imperative/HOL

DOI10.1007/978-3-319-22102-1_17zbMath1465.68290OpenAlexW1955004327MaRDI QIDQ2945637

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) General topics in the theory of algorithms (68W01) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

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, A verified SAT solver framework with learn, forget, restart, and incrementality, Automatic refinement to efficient data structures: a comparison of two approaches, Unnamed Item, Unnamed Item, Unnamed Item, Proof-producing synthesis of CakeML from monadic HOL functions, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Verified Characteristic Formulae for CakeML, For a few dollars more. Verified fine-grained algorithm analysis down to LLVM, Formal verification of an executable LTL model checker with partial order reduction, Rule-based static analysis of network protocol implementations, Efficient verified (UN)SAT certificate checking, Formalizing the Edmonds-Karp Algorithm

Uses Software

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

Cites Work

• Unnamed Item
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Mechanised Separation Algebra
• Finger trees: a simple general-purpose data structure
• Imperative Functional Programming with Isabelle/HOL
• Characteristic formulae for the verification of imperative programs
• Ynot
• Compositional shape analysis by means of bi-abduction
• Permission accounting in separation logic
• Automatic Data Refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• The Isabelle Collections Framework