Explicit Safety Property Strengthening in SAT-based Induction

Strengthening a property allows it to be falsified/verified at an earlier induction depth. In this paper, we propose new preprocessing techniques for explicitly identifying co-invariants for a given safety property which are then added to that property for faster verification. First, we employ a path-oriented decision making engine to quickly identify several states which have paths to states violating the property. Next, we generate a set of candidate co-invariants and propose an induction-based technique to learn true co-invariants among those candidates. All the learned co-invariants are minimized using resolution and added to the original property to strengthen it. Experiments show that the induction depth needed to prove many safety properties can be significantly reduced via our strengthening, thereby achieving more than an order of magnitude runtime improvements