Automated Verification of Parallel Nested DFS
From MaRDI portal
Publication:5039512
DOI10.1007/978-3-030-45190-5_14OpenAlexW3016590549MaRDI QIDQ5039512
Marieke Huisman, Jaco van de Pol, Sebastiaan J. C. Joosten, Wytse Oortwijn
Publication date: 13 October 2022
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-45190-5_14
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Automated verification of the parallel Bellman-Ford algorithm ⋮ Certifying emptiness of timed Büchi automata
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formal verification of an executable LTL model checker with partial order reduction
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- Depth-first search is inherently sequential
- Automata-theoretic techniques for modal logics of programs
- Certifying proofs for SAT-based model checking
- Verified model checking of timed automata
- Distributed breadth-first search LTL model checking
- Resource Protection Using Atomics
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- Three SCC-Based Emptiness Checks for Generalized Büchi Automata
- Dafny: An Automatic Program Verifier for Functional Correctness
- Multi-core Nested Depth-First Search
- Parallel Nested Depth-First Searches for LTL Model Checking
- Verifying Concurrent Graph Algorithms
- Handbook of Model Checking
- Improved Multi-Core Nested Depth-First Search
- Tools and Algorithms for the Construction and Analysis of Systems
- Concurrent Separation Logic and Operational Semantics
