Temporal prophecy for proving temporal properties of infinite-state systems
From MaRDI portal
Publication:2058382
DOI10.1007/s10703-021-00377-1OpenAlexW3186996227MaRDI QIDQ2058382
Oded Padon, Jochen Hoenicke, Andreas Podelski, Sharon Shoham, Mooly Sagiv, K. L. McMillan
Publication date: 8 December 2021
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2106.00966
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Inference of ranking functions for proving temporal properties by abstract interpretation
- The existence of refinement mappings
- The power of temporal proofs
- A methodology for hardware verification using compositional model checking
- On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
- Fairness modulo theory: a new approach to LTL software model checking
- Booting clock synchronization in partially synchronous systems with hybrid process and link failures
- An abstract interpretation framework for termination
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Synthesis of distributed algorithms with parameterized threshold guards
- Liveness by Invisible Invariants
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- From Shape Analysis to Termination Analysis in Linear Time
- Proving Liveness of Parameterized Programs
- Alternation for Termination
- Transition predicate abstraction and fair termination
- Ramsey vs. Lexicographic Termination Proving
- Thread modularity at many levels: a pearl in compositional verification
- Making prophecies with decision predicates
- An Abstract Domain to Infer Ordinal-Valued Ranking Functions
- Proving Liveness by Backwards Reachability
- Deductive verification in decidable fragments with Ivy
