TPA

Transition Power Abstraction (TPA) is a technique for checking safety properties of transition systems. It uses a sequence of relations that over-approximate increasingly larger number of steps of the transition relation. Its distinguishing feature is that the number of steps covered increases exponentially (not linearly).

TPA has been successfully used for detecting deep counterexamples in challenging multiphase loops.