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…