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

DOI10.1007/978-3-319-21690-4_2MaRDI QIDQ1702907zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(16)

• A compositional approach to CTL^* verification
• Temporal prophecy for proving temporal properties of infinite-state systems
• Learning to verify branching time properties
• CTL-property transformations along an incremental design process
• scientific article; zbMATH DE number 1927551 (Why is no real title available?)
• Verifying increasingly expressive temporal logics for infinite-state systems
• Efficient CTL verification via Horn constraints solving
• The virtues of idleness: a decidable fragment of resource agent logic
• Fold/unfold transformations for fixpoint logic
• Making prophecies with decision predicates
• Abstraction refinement and antichains for trace inclusion of infinite state systems
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Inference of ranking functions for proving temporal properties by abstract interpretation
• Constraint automata on infinite data trees: from \(\mathrm{CTL}(\mathbb{Z})/\mathrm{CTL}^*(\mathbb{Z})\) to decision procedures
• Constraint automata on infinite data trees: from CTL\((\mathbb{Z})\text{CTL}^*(\mathbb{Z})\) to decision procedures
• Lower-bound synthesis using loop specialization and Max-SMT

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)