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

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

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

(14)

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

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)