This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consisder 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 chekcing. 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 hte sets of predecessors resp. successors. the 'operational computation of these sets is carried out using the Dowling-Gallier procedure for HornSat.
展开▼
