Showing 2024Show all
2 papers · 1 filter
cs.PL2024
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…
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…