3 papers
cs.LO2026
Verifying First-Order Temporal Properties of Infinite-State Systems via Timers and Rankings
Raz Lotan, Neta Elad, Oded Padon +1
We present a unified deductive verification framework for first-order temporal properties based on well-founded rankings, where verification conditions are discharged using SMT sol…
cs.LO2024
Implicit Rankings for Verifying Liveness Properties in First-Order Logic
Raz Lotan, Sharon Shoham
Liveness properties are traditionally proven using a ranking function that maps system states to some well-founded set. Carrying out such proofs in first-order logic enables automa…
cs.LO2024
Proving Cutoff Bounds for Safety Properties in First-Order Logic
Raz Lotan, Eden Frenkel, Sharon Shoham
First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are par…