| Autor: |
Pnueli, Amir, Sa΄ar, Yaniv |
| Zdroj: |
Verification, Model Checking & Abstract Interpretation (9783540781622); 2008, p233-247, 15p |
| Abstrakt: |
The paper presents a new deductive rule for verifying response properties under the assumption of compassion (strong fairness) requirements. It improves on previous rules in that the premises of the new rule are all first order. We prove that the rule is sound, and present a constructive completeness proof for the case of finite-state systems. For the general case, we present a sketch of a relative completeness proof. We report about the implementation of the rule in PVS and illustrate its application on some simple but non-trivial examples. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
