Transition predicate abstraction and fair termination

Predicate abstraction is the basis of many program verifica-tion tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety prop-erties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to transition predicate abstraction. Transition predicate abstraction goes beyond the idea of finite abstract-state programs (and check-ing the absence of loops). Instead, our abstraction algorithm transforms a program into a finite abstract-transition pro-gram. Then, a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (justice and compassion). In summary, we ex-hibit principles that extend the applicability of predicate abstraction-based program verification to the full set of tem-poral properties