3 papers
cs.LO2026
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…
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…
cs.LO2024
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Eden Frenkel, Tej Chajed, Oded Padon +1
This paper lays a practical foundation for using abstract interpretation with an abstract domain that consists of sets of quantified first-order logic formulas. This abstract domai…