Channel dependence analysis for slicing Promela

Accurate channel analysis and communication dependence information is necessary for source code analysis tools to be useful in the concurrent specification and programming language domain. We present channel analysis along with an application thereof and describe its implications for the development and understanding of programs written in concurrent languages. We describe how communication dependences within a concurrent program can be computed and then used in combination with control and flow dependences to construct a representation that allows for efficient program slicing