A tractable reduction heuristic for model checking of software

We present a new model for model checking which is designed for finite state parallelized software systems. We show that the expressiveness of this model is sufficient to express interesting properties. We characterize the verification problem in terms suitable for automated algorithmic analysis. A complexity result demonstrates PSPACE-completeness of the verification problem.; We approach the problem of verification within the model by reducing the of a system with respect to the verification property. We are able to compute our automated reduction in polynomial time.