3 papers
cs.LO2024
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta Elad, Oded Padon, Sharon Shoham
First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove diff…
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…
cs.LO2024
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, su…