Communicating pushdown systems (CPDSs) are a formalism for modeling the behaviors of concurrent systems. They have been used to model concurrent C and Java programs. Once a concurrent program has been modeled as a CPDS, a reachability query is given to a CPDS model checker to determine if the property of interest is satisfied by the program model.

Our CPDS model checker implements a semi-decision procedure for answering a reachability query. For a given CPDS, the semi-decision procedure defines increasingly more-precise approximations of the reachability relation of a CPDS to determine if the query holds.

The focus of this paper is on improving the semi-decision procedure employed by the CPDS model checker. We define a new semi-decision procedure that is more precise and more efficient, and explore three new abstraction-refinement policies. When analyzing CPDSs generated from Java programs, the new policies produced median speedups of 2.4, 1.2, and 2.5, and maximum speedups of 5.4, 5.3, and 7.6.

(Click here to access the paper: PDF.)