Using the Karp-Miller Tree Construction to Analyse Concurrent Finite-State Programs
Haoxian Zhao · 2009
The formal analysis of multi-threaded programs is among the grand challenges of software verification research. In this dissertation, we consider non-recursive multi-threaded Boolean programs, the principal ingredient in predicate abstraction. We introduced a exact and complete solution for thread-state reachability analysis of concurrent Boolean programs with unbounded thread creation. We present a novel implementation of the Karp-Miller procedure for vector addition systems with states, and evaluate its performance using a substantial set of Boolean program benchmarks. We then use our technique to prove that the benchmark programs have surprisingly small reachability cutoffs. We conclude that verifying a program for the fixed cutoff-number of threads tends to be cheaper than the Karp-Miller procedure. Our results mark a first step towards truly efficient strategies for analyzing multi-threaded programs.