Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems

Temporal logic is a formal system for specifying and reasoning about propositions qualified in terms of time. It offers a unified approach to program verification as it applies to both sequential and parallel programs and provides a uniform framework for describing a system at any level of abstraction. Thus a number of automated systems have been proposed to exclusively reason about either Computation-Tree Logic (CTL) or Linear Temporal Logic (LTL) in the infinite-state setting. Unfortunately, these logics have significantly reduced expressiveness as they restrict the interplay between temporal operators and path quantifiers, thus disallowing the expression of many practical properties, for example “along some future an event occurs infinitely often”. Contrarily, CTL∗, a superset of both CTL and LTL, can facilitate the interplay between path-based and state-based reasoning. CTL∗ thus exclusively allows for the expressiveness of properties involving existential system stabilization and “possibility” properties. Until now, there have not existed automated systems that allow for the verification of such expressive CTL∗ properties over infinite-state systems. This paper proposes a method capable of such a task, thus introducing the first known fully automated tool for symbolically proving CTL∗ properties of (infinite-state) integer programs. The method uses an internal encoding that admits reasoning about the subtle interplay between the nesting of temporal operators and path quantifiers that occurs within CTL∗ proofs. A program transformation is first employed that trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We then synthesize and quantify preconditions over the transformed program that represent program states that satisfy a CTL∗ formula. This paper demonstrates the viability of our approach in practice, thus leading to a new class of fullyautomated tools capable of proving crucial properties that no tool could previously prove. Additionally, we consider the linear-past extension to CTL∗ for infinite-state systems in which the past is linear and each moment in time has a unique past. We discuss the practice of this extension and how it is further supported through the use of history variables. We have implemented our approach and report our benchmarks carried out on case studies ranging from smaller programs to demonstrate the expressiveness of CTL∗ specifications, to larger code bases drawn from device drivers and various industrial examples