Transition predicate abstraction and fair termination

11 years 1 months ago
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...
Andreas Podelski, Andrey Rybalchenko
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Andreas Podelski, Andrey Rybalchenko
Comments (0)