On automation of CTL^* verification for infinite-state systems

DOI10.1007/978-3-319-21690-4_2zbMATH Open1381.68154OpenAlexW2128803539MaRDI QIDQ1702907FDOQ1702907

Authors: Byron Cook, Heidy Khlaaf, Nir Piterman 

Publication date: 1 March 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-21690-4_2

Recommendations

• Verifying increasingly expressive temporal logics for infinite-state systems
• Fairness for Infinite-State Systems
• A compositional approach to CTL\(^*\) verification
• scientific article; zbMATH DE number 1927551
• Abstract interpretation of CTL properties

Mathematics Subject Classification ID

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

Cited In (14)

• Verifying increasingly expressive temporal logics for infinite-state systems
• Lower-bound synthesis using loop specialization and Max-SMT
• CTL-property transformations along an incremental design process
• Making prophecies with decision predicates
• Learning to verify branching time properties
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• A compositional approach to CTL\(^*\) verification
• Temporal prophecy for proving temporal properties of infinite-state systems
• Efficient CTL verification via Horn constraints solving
• Automatically verifying temporal properties of pointer programs with cyclic proof
• The virtues of idleness: a decidable fragment of resource agent logic
• Fold/unfold transformations for fixpoint logic
• Title not available (Why is that?)
• Inference of ranking functions for proving temporal properties by abstract interpretation

This page was built for publication: On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems

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