Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

Jason R. Koenig, Oded Padon, Sharon Shoham +1

We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified in…