In this paper we introduce the first known tool for symbolically proving
-CTL properties of (infinite-state) integer programs. Our solution is based on a reduction to existing techniques for fairness-free CTL model checking via the use of infinite non-deterministic branching to symbolically partition fair from unfair executions. We show the viability of our approach in practice using examples drawn from device drivers and algorithms utilizing shared resources.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten