Invariant Inference With Provable Complexity From the Monotone Theory

Yotam M. Y. Feldman, Sharon Shoham

Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, b…