Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property
Neta Elad, Sharon Shoham
Recently, symbolic structures were proposed as finite representations of potentially infinite first-order structures, where Linear Integer Arithmetic terms and formulas define the…
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.LO2025
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Neta Elad, Adithya Murali, Sharon Shoham
For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and p…