Parallel Explicit Model Checking for Generalized Büchi Automata

DOI10.1007/978-3-662-46681-0_56MaRDI QIDQ5194963zbMATH OpenOpenAlexFDO

Authors E. Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

Publication date 17 September 2019

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-662-46681-0_56

zbMATH Keywords

good speedupmodel checkingmultiple threadprototype implementationstrongly connect component

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parallelizing a symbolic compositional model-checking algorithm
• scientific article; zbMATH DE number 1705169
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)
• scientific article; zbMATH DE number 1796122
• Efficient model checking algorithms for computation tree logic and their application to the verification of parallel programs
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 1746649

Cited in

(11)

• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• LTL to self-loop alternating automata with generic acceptance and back
• Finding strongly connected components of simple digraphs based on granulation strategy
• Model checking with multi-threaded IC3 portfolios
• Three SCC-based emptiness checks for generalized Büchi automata
• Model Checking Software
• Strength-based decomposition of the property Büchi automaton for faster model checking
• Parallelizing a symbolic compositional model-checking algorithm
• Model Checking Software
• Nested emptiness search for generalized Büchi automata
• Parallel Graph-Based Stateless Model Checking

This page was built for publication: Parallel Explicit Model Checking for Generalized Büchi Automata

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