scientific article; zbMATH DE number 7649962
From MaRDI portal
Publication:5875421
DOI10.4230/LIPIcs.ITP.2019.13MaRDI QIDQ5875421
Stephan Merz, Jean-Jacques Levy, Cyril Cohen, Laurent Théry, Ran Chen
Publication date: 3 February 2023
Full work available at URL: https://arxiv.org/abs/1810.11979
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Local Reasoning for Global Graph Properties ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
Uses Software
Cites Work
- Unnamed Item
- Isabelle
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- A semi-automatic proof of strong connectivity
- Hammer for Coq: automation for dependent type theory
- Refinement to imperative HOL
- A formal proof of the minor-exclusion property for treewidth-two graphs
- A simplified correctness proof for a well-known algorithm computing strongly connected components.
- A graph library for Isabelle
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Extending Sledgehammer with SMT solvers
- From Proposition to Program
- Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
- Hoare-Style Verification of Graph Programs
- Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
- The ramifications of sharing in data structures
- Verifying Concurrent Graph Algorithms
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Characteristic formulae for the verification of imperative programs
- Depth-First Search and Linear Graph Algorithms
- Partiality and recursion in interactive theorem provers – an overview
- Automated Deduction – CADE-19
This page was built for publication:
