Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
Abstract elided by the publisher.
Related papers
- Reducing liveness to safety in first-order logic POPL 2018
- Sound Verification Procedures for Temporal Properties of Infinite-State Systems CAV 2021
- Implicit Rankings for Verifying Liveness Properties in First-Order Logic TACAS 2025
- Verifying Infinite State Processes with Sequential and Parallel Composition POPL 1995
- Bounded model checking of signal temporal logic properties using syntactic separation POPL 2019
- Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis POPL 2025
- Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs POPL 2025
- Parameterized Infinite-State Reactive Synthesis POPL 2026