Loading...
Please wait, while we are loading the content...
Similar Documents
Transition predicate abstraction and fair termination (2005)
| Content Provider | CiteSeerX |
|---|---|
| Author | Rybalchenko, Andrey Podelski, Andreas |
| Abstract | 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 properties 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 checking the absence 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 (impartiality, justice, and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties. |
| File Format | |
| Publisher Date | 2005-01-01 |
| Access Restriction | Open |
| Subject Keyword | Known Way Predicate Abstraction-based Program Verification Many Program Verification Tool Predicate Abstraction Safety Property Inherent Limitation Automated Method Full Set Liveness Property Transition Predicate Abstraction Full Fairness Assumption Temporal Property Ecole Polytechnique Rale Special Popl Issue Abstraction Algorithm Second Algorithm Check Fair Termination Finite Abstract-transition Program Finite-state Abstraction Finite Abstract-state Program |
| Content Type | Text |
