Fairness for Infinite-State Systems

In this paper we introduce the first known tool for symbolically proving fair-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.