Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation

DOI10.1007/978-3-642-04761-9_27zbMath1262.68132OpenAlexW1569724714MaRDI QIDQ3648712

Gianfranco Ciardo, Yang Zhao

Publication date: 1 December 2009

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04761-9_27

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (3)

Symbolic Termination and Confluence Checking for ECA Rules ⋮ Saturation Enhanced with Conditional Locality: Application to Petri Nets ⋮ Component-wise incremental LTL model checking

Uses Software

• NuSMV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• NuSMV: A new symbolic model checker
• Exploiting interleaving semantics in symbolic state-space generation
• Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams
• Graph-Based Algorithms for Boolean Function Manipulation
• Correct Hardware Design and Verification Methods
• Computer Aided Verification

This page was built for publication: Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation