On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
From MaRDI portal
Publication:1702907
DOI10.1007/978-3-319-21690-4_2zbMath1381.68154OpenAlexW2128803539MaRDI QIDQ1702907
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
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items
Lower-bound synthesis using loop specialization and Max-SMT, Inference of ranking functions for proving temporal properties by abstract interpretation, The virtues of idleness: a decidable fragment of resource agent logic, Fold/Unfold Transformations for Fixpoint Logic, Abstraction refinement and antichains for trace inclusion of infinite state systems, Automatically verifying temporal properties of pointer programs with cyclic proof, Temporal prophecy for proving temporal properties of infinite-state systems
