Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
Abstract elided by the publisher.
Related papers
- Infinite-State Liveness Checking with rlive CAV 2025
- Reducing liveness to safety in first-order logic POPL 2018
- Implicit Rankings for Verifying Liveness Properties in First-Order Logic TACAS 2025
- Avoiding the Shoals - A New Approach to Liveness Checking CAV 2024
- Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems CAV 2021
- Sound Verification Procedures for Temporal Properties of Infinite-State Systems CAV 2021
- IC3 Modulo Theories via Implicit Predicate Abstraction TACAS 2014
- Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results TOPLAS 1999