Verifying Liveness Properties by Verifying Safety Properties
Abstract elided by the publisher.
Related papers
- Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits CAV 1991
- Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions POPL 2024
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms POPL 2017
- Reducing liveness to safety in first-order logic POPL 2018
- Verifying LTL Properties of Hybrid Systems with K-Liveness CAV 2014
- HyperLasso: Bounded Model Checking of ∀+∃>+-Liveness Hyperproperties CAV 2026
- LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs PLDI 2024
- A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems TACAS 2023