Transition predicate abstraction and fair termination

on Predicate Abstraction and Fair Termination Andreas Podelski Andrey Rybalchenko Max-Planck-Institut f?ur Informatik Saarbr?ucken, Germany Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety propas to manually annotate the finite-state abstraction gram. We extend predicate abstraction to transition e abstraction. Transition predicate abstraction goes beyond the idea of finite abstract-state programs (and checkabsence of loops). Instead, our abstraction algorithm transforms a program into a finite abstract-transition program. 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 exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of tempor...

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Andreas Podelski, Andrey Rybalchenko
• Keywords: Fair Termination, POPL 2005, Predicate Abstraction, Programming Languages, Transition Predicate Abstraction