Distributed breadth-first search LTL model checking

DOI10.1007/S10703-006-0009-YMaRDI QIDQ2431772zbMATH OpenOpenAlexFDO

Authors J. Barnat, I. Černá

Publication date 24 October 2006

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-006-0009-y

zbMATH Keywords

Breadth-first searchDistributed memoryLTL model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Distributed explicit bounded LTL model checking
• Bounded model checking distributed temporal logic
• Efficient distributed SAT and SAT-based distributed bounded model checking
• Parallel nested depth-first searches for LTL model checking
• scientific article; zbMATH DE number 1744967
• scientific article; zbMATH DE number 2081097
• Parameterized verification and model checking for distributed broadcast protocols

Cites work

• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 2081097 (Why is no real title available?)
• scientific article; zbMATH DE number 1746648 (Why is no real title available?)
• scientific article; zbMATH DE number 1744967 (Why is no real title available?)
• Automata-theoretic techniques for modal logics of programs
• Distributed partial order reduction of state spaces
• Formal Methods in Computer-Aided Design
• Mathematical Foundations of Computer Science 2003
• The temporal semantics of concurrent programs

Cited in

(14)

• Cluster-Based LTL Model Checking of Large Systems
• Distributed explicit bounded LTL model checking
• BFS-based model checking of linear-time properties with an application on GPUs
• Formal Methods in Computer-Aided Design
• Automated verification of parallel nested DFS
• Multi-core nested depth-first search
• scientific article; zbMATH DE number 1982197 (Why is no real title available?)
• scientific article; zbMATH DE number 2081097 (Why is no real title available?)
• Parallel nested depth-first searches for LTL model checking
• Improved multi-core nested depth-first search
• Bounded model checking distributed temporal logic
• scientific article; zbMATH DE number 1744967 (Why is no real title available?)
• How to order vertices for distributed LTL model-checking based on accepting predecessors
• Random walk based heuristic algorithms for distributed memory model checking

Describes a project that uses

Uses Software

• DiVinE
• SPIN

This page was built for publication: Distributed breadth-first search LTL model checking

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