A compositional approach to CTL\(^*\) verification

DOI10.1016/j.tcs.2004.09.023zbMath1079.68059OpenAlexW2078078820MaRDI QIDQ1770366

Yonit Kesten, Amir Pnueli

Publication date: 6 April 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.09.023

zbMATH Keywords

deductive verificationsymbolic model-checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)

Related Items (10)

Automatic discovery of fair paths in infinite-state transition systems ⋮ Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ Unnamed Item ⋮ Deductive verification of alternating systems ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Proving the Refuted: Symbolic Model Checkers as Proof Generators ⋮ Checking Temporal Properties of Discrete, Timed and Continuous Behaviors ⋮ MODULAR RANKING ABSTRACTION ⋮ \textsc{LTL} falsification in infinite-state systems ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain

Uses Software

• STeP

Cites Work

• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Completing the temporal picture
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Modalities for model checking: Branching time logic strikes back
• Verification by augmented finitary abstraction
• Verification of concurrent programs: The automata-theoretic framework
• Model checking with strong fairness
• An axiomatization of full Computation Tree Logic
• “Sometimes” and “not never” revisited
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A compositional approach to CTL\(^*\) verification