Fairness for Infinite-State Systems

Abstract

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.