Abstract

The formal analysis of multi-threaded programs is among the grand challenges of software verification research. In this talk, I describe our recent and ongoing work on analyzing parameterized finite-state programs, such as non-recursive multi-threaded Boolean programs, a principal ingredient in predicate abstraction. I begin with a scalable method for analyzing the reachability of program locations in programs executed by a bounded number of threads. This method, being based on counter abstraction, extends in principle to unbounded thread counts, but suffers in practice from the high complexity of coverability and reachability analyses for certain types of counter machines. A different approach to program location reachability rests on the assumption that in practical parametric program settings, a small “cutoff” number of threads suffice to generate all reachable program locations. While this assumption is widely considered to be safe, its practical usefulness hinges on how accurately we are able to estimate the cutoff of a given program. I present a new method that analyses the reachable state space of a replicated finite-state program for increasing thread counts, until a condition emerges that allows us to conclude that the cutoff thread count has been reached. Completeness of this method is achieved by resorting to traditional coverability analyses in corner cases. The result is a precise and efficient program location reachability method for non-recursive concurrent Boolean programs run by arbitrarily many threads.