1 citations · 1 across the 8 of their papers we have counts for
9 papers
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…
Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
Eden Frenkel, Kenneth L. McMillan, Oded Padon +1
We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines ru…
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…
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…
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
Takeshi Tsukada, Hiroshi Unno, Oded Padon +1
Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an i…
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…
Axe 'Em: Eliminating Spurious States with Induction Axioms
Neta Elad, Sharon Shoham
First-order logic (FOL) has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as…
Hyperproperty-Preserving Register Specifications (Extended Version)
Yoav Ben Shimon, Ori Lahav, Sharon Shoham
Reasoning about hyperproperties of concurrent implementations, such as the guarantees these implementations provide to randomized client programs, has been a long-standing challeng…
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…