Refinement Monadic
From MaRDI portal
swMATH28551MaRDI QIDQ40265FDOQ40265
Author name not available (Why is that?)
Official website: https://www.isa-afp.org/entries/Refine_Monadic.html
Cited In (32)
- Transition_Systems_and_Automata
- Formal verification of an executable LTL model checker with partial order reduction
- Refinement to imperative HOL
- A verified ODE solver and the Lorenz attractor
- Netsoft
- Autoref
- CFML
- MLton
- CAVA Automata Library
- CAVA
- Dijkstra Shortest Path
- Edmonds-Karp
- Collections
- Flow Networks
- Affine Arithmetic
- CAVA LTL Modelchecker
- Dictionary Construction
- Separation Logic
- Gabow SCC
- LTL_to_DRA
- Native Word
- Imperative Refinement
- Stuttering Equivalence
- Program-Conflict-Analysis
- Boolean_Expression_Checkers
- Prpu_Maxflow
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Formalizing the Edmonds-Karp algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
This page was built for software: Refinement Monadic
