Applying data refinement for monadic programs to Hopcroft's algorithm
From MaRDI portal
Publication:2914741
Recommendations
Cited in
(23)- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Refinement to Imperative/HOL
- From LCF to Isabelle/HOL
- Effect polymorphism in higher-order logic (proof pearl)
- Formalizing the Edmonds-Karp algorithm
- Data refinement in Isabelle/HOL
- Equational Reasoning with Applicative Functors
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Formal verification of an executable LTL model checker with partial order reduction
- Efficient verified (UN)SAT certificate checking
- Automatic refinement to efficient data structures: a comparison of two approaches
- Formalization and execution of linear algebra: from theorems to algorithms
- Effect polymorphism in higher-order logic (proof pearl)
- Flexible Correct-by-Construction Programming
- 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?)
- Verified iptables firewall analysis and verification
- Refinement to imperative HOL
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Efficient Verified Implementation of Introsort and Pdqsort
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
Describes a project that uses
Uses Software
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)
