Distributed breadth-first search LTL model checking

DOI10.1007/S10703-006-0009-YzbMATH Open1102.68503OpenAlexW2000162135MaRDI QIDQ2431772FDOQ2431772

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

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

zbMATH Keywords

Breadth-first searchDistributed memoryLTL model checking

Mathematics Subject Classification ID

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

Cites Work

• The temporal semantics of concurrent programs
• Title not available (Why is that?)
• Automata-theoretic techniques for modal logics of programs
• Formal Methods in Computer-Aided Design
• Title not available (Why is that?)
• Distributed partial order reduction of state spaces
• Mathematical Foundations of Computer Science 2003
• Title not available (Why is that?)
• Title not available (Why is that?)

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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Bounded model checking distributed temporal logic
• Parallel nested depth-first searches for LTL model checking
• Improved multi-core nested depth-first search
• Title not available (Why is that?)
• How to order vertices for distributed LTL model-checking based on accepting predecessors
• Random walk based heuristic algorithms for distributed memory model checking

Uses Software

• SPIN
• DiVinE

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)