Efficient algorithms for pre* and post* on interprocedural parallel flow graphs

This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consider the generalization to the case of parallel programs. We give algorithms that compute the sets of backward resp. forward reachable configurations for parallel flow graph systems in linear time in the size of the graph viz. the program. These operations are important in dataflow analysis and in model checking. In our method, we first model configurations as terms (viz. trees) in the process algebra PA that can express call stack operations and parallelism. We then give a `declarative' Horn-clause specification of the sets of predecessors resp. successors. The `operational' computation of these sets is carried out using the Dowling-Gallier procedure for HornSat.