TR-IIS-05-009    Fulltext

Abstract

In this paper, we use the reflection of rewriting logic to analyze a bounded local model checker for infinite-state systems formally. We introduce three-valued logic in a local model checking algorithm to formalize aborted verification. To improve its efficiency, several optimizations are introduced in the algorithm. We show how to exploit the reflection of rewriting logic and model check our bounded local model checker in rewriting logic formally.