Observation: IC3 and interpolation find candidates that are guaranteed to exclude some failure, but may not be inductive. Abstract interpretation & acceleration find candidates that are guaranteed to be inductive & initial, but may not prove safety. We can tune our fitness functions to search in these 3 dimensions (or more) -- try to find a unifying theory of how all these procedures work, parameterised in some way that allows us to turn a dial from interpolation to abstract interpretation, via Kalashnikov.
Observation: IC3 and interpolation find candidates that are guaranteed to exclude some failure, but may not be inductive. Abstract interpretation & acceleration find candidates that are guaranteed to be inductive & initial, but may not prove safety. We can tune our fitness functions to search in these 3 dimensions (or more) -- try to find a unifying theory of how all these procedures work, parameterised in some way that allows us to turn a dial from interpolation to abstract interpretation, via Kalashnikov.