Applying data refinement for monadic programs to Hopcroft's algorithm

DOI10.1007/978-3-642-32347-8_12zbMATH Open1360.68757OpenAlexW77329694MaRDI QIDQ2914741FDOQ2914741

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

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

Mathematics Subject Classification ID

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

Cited In (23)

• 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
• 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
• Formalization and execution of linear algebra: from theorems to algorithms
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalizing the Edmonds-Karp algorithm
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

Uses Software

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

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)