A compositional approach to CTL^* verification

DOI10.1016/J.TCS.2004.09.023MaRDI QIDQ1770366zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4085004 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 2081113 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• An axiomatization of full computation tree logic
• Completing the temporal picture
• Modalities for model checking: Branching time logic strikes back
• Model checking with strong fairness
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Theories of automata on \(\omega\)-tapes: a simplified approach
• Verification by augmented finitary abstraction
• Verification of concurrent programs: The automata-theoretic framework
• “Sometimes” and “not never” revisited

Cited in

(22)

• scientific article; zbMATH DE number 6708298 (Why is no real title available?)
• MODULAR RANKING ABSTRACTION
• \textsc{LTL} falsification in infinite-state systems
• Automatic discovery of fair paths in infinite-state transition systems
• “ReLIC: Reduced Logic Inference for Composition” for Quantifier Elimination based Compositional Reasoning
• 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
• scientific article; zbMATH DE number 1231598 (Why is no real title available?)
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Proving the existence of fair paths in infinite-state systems
• CTL model checking in deduction modulo
• 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
• Deductive verification of alternating systems
• Completeness and Decidability Results for CTL in Coq
• On the computation of counterexamples in compositional nonblocking verification
• scientific article; zbMATH DE number 1927551 (Why is no real title available?)

Describes a project that uses

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)