Automated verification of parallel nested DFS

DOI10.1007/978-3-030-45190-5_14MaRDI QIDQ5039512zbMATH OpenOpenAlexFDO

Authors Wytse Oortwijn, Marieke Huisman, Sebastiaan J. C. Joosten, Jaco van de Pol

Publication date 13 October 2022

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45190-5_14

Mathematics Subject Classification ID

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)

Recommendations

• Automated verification of the parallel Bellman-Ford algorithm
• Parallel nested depth-first searches for LTL model checking
• scientific article; zbMATH DE number 1069483
• Multi-core nested depth-first search
• Improved multi-core nested depth-first search

Cites work

• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 1069483 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A semantics for concurrent separation logic
• Automata-theoretic techniques for modal logics of programs
• Certifying proofs for SAT-based model checking
• Concurrent separation logic and operational semantics
• Dafny: an automatic program verifier for functional correctness
• Depth-first search is inherently sequential
• Distributed breadth-first search LTL model checking
• Formal verification of an executable LTL model checker with partial order reduction
• Handbook of model checking
• Improved multi-core nested depth-first search
• Multi-core nested depth-first search
• Parallel nested depth-first searches for LTL model checking
• Resource protection using atomics. Patterns and verification
• Resources, concurrency, and local reasoning
• Three SCC-based emptiness checks for generalized Büchi automata
• Tools and Algorithms for the Construction and Analysis of Systems
• Verified model checking of timed automata
• Verifying concurrent graph algorithms
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(5)

• Recognition of DFS trees: Sequential and parallel algorithms with refined verifications
• Certifying emptiness of timed Büchi automata
• BFS-based model checking of linear-time properties with an application on GPUs
• Automated Verification of Concurrent Search Structures
• Automated verification of the parallel Bellman-Ford algorithm

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Viper
• VeriFast
• LTSmin
• z3
• SPIN
• Dafny
• Coq

This page was built for publication: Automated verification of parallel nested DFS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5039512)