Temporal prophecy for proving temporal properties of infinite-state systems (Q2058382): Difference between revisions

@@ Property / author @@
-K. L. McMillan
@@ Property / author: K. L. McMillan / rank @@
-Normal rank
@@ Property / author @@
+K. L. McMillan
@@ Property / author: K. L. McMillan / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ivy
@@ Property / describes a project that uses: Ivy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ivy
@@ Property / describes a project that uses: Ivy / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+AProVE
@@ Property / describes a project that uses: AProVE / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3186996227
@@ Property / OpenAlex ID: W3186996227 / rank @@
+Normal rank
@@ Property / cites work @@
+The power of temporal proofs
@@ Property / cites work: The power of temporal proofs / rank @@
+Normal rank
@@ Property / cites work @@
+The existence of refinement mappings
@@ Property / cites work: The existence of refinement mappings / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Liveness by Backwards Reachability
@@ Property / cites work: Proving Liveness by Backwards Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
+Normal rank
@@ Property / cites work @@
+Making prophecies with decision predicates
@@ Property / cites work: Making prophecies with decision predicates / rank @@
+Normal rank
@@ Property / cites work @@
+Ramsey vs. Lexicographic Termination Proving
@@ Property / cites work: Ramsey vs. Lexicographic Termination Proving / rank @@
+Normal rank
@@ Property / cites work @@
+An abstract interpretation framework for termination
+Normal rank
@@ Property / cites work @@
+Fairness modulo theory: a new approach to LTL software model checking
+Normal rank
@@ Property / cites work @@
+Liveness by Invisible Invariants
@@ Property / cites work: Liveness by Invisible Invariants / rank @@
+Normal rank
@@ Property / cites work @@
+Proving Liveness of Parameterized Programs
@@ Property / cites work: Proving Liveness of Parameterized Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Alternation for Termination
@@ Property / cites work: Alternation for Termination / rank @@
+Normal rank
@@ Property / cites work @@
+Thread modularity at many levels: a pearl in compositional verification
+Normal rank
@@ Property / cites work @@
+Q4484481
@@ Property / cites work: Q4484481 / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesis of distributed algorithms with parameterized threshold guards
+Normal rank
@@ Property / cites work @@
+From Shape Analysis to Termination Analysis in Linear Time
+Normal rank
@@ Property / cites work @@
+A methodology for hardware verification using compositional model checking
+Normal rank
@@ Property / cites work @@
+Deductive verification in decidable fragments with Ivy
+Normal rank
@@ Property / cites work @@
+Q2754094
@@ Property / cites work: Q2754094 / rank @@
+Normal rank
@@ Property / cites work @@
+Transition Invariants and Transition Predicate Abstraction for Program Termination
+Normal rank
@@ Property / cites work @@
+Transition predicate abstraction and fair termination
+Normal rank
@@ Property / cites work @@
+An Abstract Domain to Infer Ordinal-Valued Ranking Functions
+Normal rank
@@ Property / cites work @@
+Inference of ranking functions for proving temporal properties by abstract interpretation
+Normal rank
@@ Property / cites work @@
+Booting clock synchronization in partially synchronous systems with hybrid process and link failures
+Normal rank