Applying data refinement for monadic programs to Hopcroft's algorithm

DOI10.1007/978-3-642-32347-8_12MaRDI QIDQ2914741zbMATH OpenOpenAlexFDO

Authors Peter Lammich, Thomas Tuerk

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-32347-8_12

Mathematics Subject Classification ID

Theory of programming languages (68N15) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatic Data Refinement
• Refinement to imperative HOL
• Refinement to Imperative/HOL
• Automatic refinement to efficient data structures: a comparison of two approaches
• Data refinement in Isabelle/HOL

Cited in

(27)

• Formal verification of an executable LTL model checker with partial order reduction
• Flexible Correct-by-Construction Programming
• A formalisation of the Myhill-Nerode theorem based on regular expressions
• Refinement to imperative HOL
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Efficient verified (UN)SAT certificate checking
• Fast and verified UNSAT certificate checking
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• A formal correctness proof of Edmonds' blossom shrinking algorithm
• Refinement to Imperative/HOL
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Equational Reasoning with Applicative Functors
• Formalization and execution of linear algebra: from theorems to algorithms
• A formal analysis of capacity scaling algorithms for minimum cost flows
• Simplified and verified: a second look at a proof-producing union-find algorithm
• Data refinement in Isabelle/HOL
• From LCF to Isabelle/HOL
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)
• Verified iptables firewall analysis and verification
• Automatic refinement to efficient data structures: a comparison of two approaches
• Efficient Verified Implementation of Introsort and Pdqsort
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• scientific article; zbMATH DE number 7649972 (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

• DiskPaxos
• Tree Automata
• Archive Formal Proofs
• Collections
• GUItar
• FAdo
• Scala
• Isabelle/HOL
• TkWinHOL

This page was built for publication: Applying data refinement for monadic programs to Hopcroft's algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914741)