Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm

DOI10.1007/978-3-642-32347-8_12zbMath1360.68757OpenAlexW77329694MaRDI QIDQ2914741

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

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

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