Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
From MaRDI portal
Publication:2914741
DOI10.1007/978-3-642-32347-8_12zbMATH Open1360.68757OpenAlexW77329694MaRDI QIDQ2914741FDOQ2914741
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
Theory of programming languages (68N15) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (22)
- 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
- Formalizing the Edmonds-Karp Algorithm
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- Efficient verified (UN)SAT certificate checking
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Title not available (Why is that?)
- Refinement to Imperative/HOL
- Equational Reasoning with Applicative Functors
- 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
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
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)
