Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
From MaRDI portal
Publication:2914741
DOI10.1007/978-3-642-32347-8_12zbMath1360.68757OpenAlexW77329694MaRDI QIDQ2914741
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
Formal languages and automata (68Q45) Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Efficient Verified Implementation of Introsort and Pdqsort, Formalization and Execution of Linear Algebra: From Theorems to Algorithms, Verified iptables firewall analysis and verification, Refinement to Imperative/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Flexible Correct-by-Construction Programming, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, For a few dollars more. Verified fine-grained algorithm analysis down to LLVM, Refinement to imperative HOL, Formal verification of an executable LTL model checker with partial order reduction, Effect polymorphism in higher-order logic (proof pearl), From LCF to Isabelle/HOL, Effect polymorphism in higher-order logic (proof pearl), Efficient verified (UN)SAT certificate checking, Formalizing the Edmonds-Karp Algorithm, Equational Reasoning with Applicative Functors, A formalisation of the Myhill-Nerode theorem based on regular expressions
Uses Software
