CTL model checking on a shared-memory architecture

DOI10.1007/S10703-006-0008-ZMaRDI QIDQ2431771zbMATH OpenOpenAlexFDO

Authors Cornelia P. Inggs, Howard Barringer

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-0008-z

zbMATH Keywords

AutomataModel checkingMultiprocessorsParallel processingShared memory

Mathematics Subject Classification ID

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

Recommendations

• CTL^* model checking on a shared-memory architecture
• Effective state exploration for model checking on a shared memory architecture
• An experiment on parallel model checking of a CTL fragment
• scientific article; zbMATH DE number 2188504
• Model Checking CTL is Almost Always Inherently Sequential

Cites work

• Distributed explicit bounded LTL model checking
• scientific article; zbMATH DE number 1670766 (Why is no real title available?)
• scientific article; zbMATH DE number 1670779 (Why is no real title available?)
• scientific article; zbMATH DE number 1705169 (Why is no real title available?)
• scientific article; zbMATH DE number 1982197 (Why is no real title available?)
• scientific article; zbMATH DE number 1746649 (Why is no real title available?)
• scientific article; zbMATH DE number 1744967 (Why is no real title available?)
• scientific article; zbMATH DE number 1798187 (Why is no real title available?)
• scientific article; zbMATH DE number 2087626 (Why is no real title available?)
• scientific article; zbMATH DE number 2090578 (Why is no real title available?)
• Practical CTL* model checking: Should SPIN be extended?
• Using assumptions to distribute alternation free {\(\mu\)}-calculus model checking
• Using assumptions to distribute CTL model checking

Cited in

(11)

• Effective state exploration for model checking on a shared memory architecture
• Load balancing parallel explicit state model checking
• CTL^* model checking on a shared-memory architecture
• A stack-slicing algorithm for multi-core model checking
• Distributed verification of multi-threaded C++ programs
• Measuring and evaluating parallel state-space exploration algorithms
• scientific article; zbMATH DE number 1982197 (Why is no real title available?)
• An experiment on parallel model checking of a CTL fragment
• Parallelizing a symbolic compositional model-checking algorithm
• A Multi-Core Solver for Parity Games
• Model Checking Software

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: CTL model checking on a shared-memory architecture

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