Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
From MaRDI portal
- A Brief Overview of HOL4
- A formally verified compiler back-end
- A Powerdomain Construction
- A strong-connectivity algorithm and its applications in data flow analysis
- A theoretical basis for stepwise refinement and the programming calculus
- A transitive closure algorithm
- Adaptive solutions to the mutual exclusion problem
- Algorithms for dense graphs and networks on the random access computer
- An axiomatic basis for computer programming
- An O(n \text{log} n) implementation of the standard method for minimizing n-state finite automata
- Animating the formalised semantics of a Java-like language
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Around Hopcroft’s Algorithm
- Automatic Data Refinement
- Code generation via higher-order rewrite systems
- Computer aided verification. 13th international conference, CAV 2001, Paris, France, July 18--22, 2001. Proceedings
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Data Refinement
- Data refinement in Isabelle/HOL
- Depth-First Search and Linear Graph Algorithms
- Efficient determination of the transitive closure of a directed graph
- Encoding, decoding and data refinement
- Enumeration and generation with a string automata representation
- Formal Certification of a Resource-Aware Language Implementation
- Formalizing the Logic-Automaton Connection
- FST TCS 2001: Foundations of software technology and theoretical computer science. 21st conference, Bangalore, India, December 13--15, 2001. Proceedings
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Imperative Functional Programming with Isabelle/HOL
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle/HOL. A proof assistant for higher-order logic
- Model Checking Software
- Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
- More efficient on-the-fly LTL verification with Tarjan's algorithm
- Path-based depth-first search for strong and biconnected components
- Proof of correctness of data representations
- Proof-producing synthesis of ML from higher-order logic
- Reasoning about infinite computations
- Refinement Calculus
- Refinement concepts formalised in higher order logic
- Secure Microkernels, State Monads and Scalable Refinement
- The B-Book
- The HOL-Omega Logic
- The Isabelle collections framework
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- The normal number of prime factors of a number n.
- Theory Is Forever
- Three SCC-based emptiness checks for generalized Büchi automata
- Tools and Algorithms for the Construction and Analysis of Systems
- Toward a verified relational database management system
- Verified efficient implementation of Gabow's strongly connected component algorithm
Cited in
(3)
This page was built for software: Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
