Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647): Difference between revisions

@@ Property / describes a project that uses @@
+Isar
@@ Property / describes a project that uses: Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Netsoft
@@ Property / describes a project that uses: Netsoft / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Dijkstra Shortest Path
@@ Property / describes a project that uses: Dijkstra Shortest Path / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Gabow SCC
@@ Property / describes a project that uses: Gabow SCC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+WhyML
@@ Property / describes a project that uses: WhyML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Why3
@@ Property / describes a project that uses: Why3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+DIMACS
@@ Property / describes a project that uses: DIMACS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MLton
@@ Property / describes a project that uses: MLton / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Separation Logic
@@ Property / describes a project that uses: Separation Logic / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Edmonds-Karp
@@ Property / describes a project that uses: Edmonds-Karp / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Refinement Monadic
@@ Property / describes a project that uses: Refinement Monadic / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Flow Networks
@@ Property / describes a project that uses: Flow Networks / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Amortized Complexity
@@ Property / describes a project that uses: Amortized Complexity / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2775427311
@@ Property / OpenAlex ID: W2775427311 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Characteristic formulae for the verification of imperative programs
+Normal rank
@@ Property / cites work @@
+Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
+Normal rank
@@ Property / cites work @@
+A semi-automatic proof of strong connectivity
@@ Property / cites work: A semi-automatic proof of strong connectivity / rank @@
+Normal rank
@@ Property / cites work @@
+On implementing the push-relabel method for the maximum flow problem
+Normal rank
@@ Property / cites work @@
+Q3651735
@@ Property / cites work: Q3651735 / rank @@
+Normal rank
@@ Property / cites work @@
+Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Maximal Flow Through a Network
@@ Property / cites work: Maximal Flow Through a Network / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to the maximum-flow problem
@@ Property / cites work: A new approach to the maximum-flow problem / rank @@
+Normal rank
@@ Property / cites work @@
+Bridging the Gap: Automatic Verified Abstraction of C
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4276004
@@ Property / cites work: Q4276004 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial and nested recursive function definitions in higher-order logic
+Normal rank
@@ Property / cites work @@
+Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
+Normal rank
@@ Property / cites work @@
+Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
+Normal rank
@@ Property / cites work @@
+Refinement to Imperative/HOL
@@ Property / cites work: Refinement to Imperative/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing the Edmonds-Karp Algorithm
@@ Property / cites work: Formalizing the Edmonds-Karp Algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Alternative Aggregates in Mizar
@@ Property / cites work: Alternative Aggregates in Mizar / rank @@
+Normal rank
@@ Property / cites work @@
+Amortized Complexity Verified
@@ Property / cites work: Amortized Complexity Verified / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+A graph library for Isabelle
@@ Property / cites work: A graph library for Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Program development by stepwise refinement
@@ Property / cites work: Program development by stepwise refinement / rank @@
+Normal rank
@@ Property / cites work @@
+The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
+Normal rank