A compositional approach to CTL^* verification

DOI10.1016/J.TCS.2004.09.023zbMATH Open1079.68059OpenAlexW2078078820MaRDI QIDQ1770366FDOQ1770366

Authors: 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

Recommendations

• A Sound and Complete Deductive System for CTL* Verification
• scientific article; zbMATH DE number 1927551
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Distributed Computing - IWDC 2004
• CTL model checking in deduction modulo

zbMATH Keywords

deductive verificationsymbolic model-checking

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (22)

• MODULAR RANKING ABSTRACTION
• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning
• \textsc{LTL} falsification in infinite-state systems
• Automatic discovery of fair paths in infinite-state transition systems
• Formula-dependent equivalence for compositional CTL model checking
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets
• Title not available (Why is that?)
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• CTL model checking in deduction modulo
• Proving the existence of fair paths in infinite-state systems
• Proving the refuted: symbolic model checkers as proof generators
• Proof-based verification approaches for dynamic properties: application to the information system domain
• Efficient CTL verification via Horn constraints solving
• A Sound and Complete Deductive System for CTL* Verification
• Compositional Verification and 3-Valued Abstractions Join Forces
• Completeness and Decidability Results for CTL in Coq
• Deductive verification of alternating systems
• On the computation of counterexamples in compositional nonblocking verification
• Title not available (Why is that?)
• Title not available (Why is that?)

Uses Software

• STeP

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

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