CUDA accelerated LTL model checking -- revisited

DOI10.4230/OASICS.MEMICS.2010.1MaRDI QIDQ2917270zbMATH OpenOpenAlexFDO

Authors Petr Bauch, Milan Češka

Publication date 28 September 2012

Full work available at URL https://www.muni.cz/vyzkum/publikace/935862

zbMATH Keywords

CUDALTL model checkingOWCTY

Mathematics Subject Classification ID

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

Recommendations

• A design of GPU-based quantitative model checking
• Parallel nested depth-first searches for LTL model checking
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Hardware acceleration for model checking
• Parallel model checking for \texttt{LTL}, \texttt{CTL}\(^*\), and \(L^2_{\mu}\)

Cited in

(1)

• A design of GPU-based quantitative model checking

Describes a project that uses

Uses Software

• DiVinE

This page was built for publication: CUDA accelerated LTL model checking -- revisited

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