BFS-based model checking of linear-time properties with an application on GPUs

DOI10.1007/978-3-319-41540-6_26MaRDI QIDQ4633562zbMATH OpenOpenAlexFDO

Authors Anton Wijs

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41540-6_26

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Recommendations

• Parallel nested depth-first searches for LTL model checking
• Distributed breadth-first search LTL model checking
• Automated verification of parallel nested DFS
• Model checking \(\omega \)-regular properties with decoupled search
• Multi-core nested depth-first search

Cited in

(3)

• A design of GPU-based quantitative model checking
• Preserving provability over GPU program optimizations with annotation-aware transformations
• Implementing a CTL model checker with \(\mu \mathcal{G}\), a language for programming graph neural networks

This page was built for publication: BFS-based model checking of linear-time properties with an application on GPUs

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