Static Analysis of IMC

In this work we use a subtype of Data Flow Analysis on systems defined by finite-state process algebras with CSP-type synchronisation - in particular, on our variant of IMC with a more permissive syntax, i.e. with a possibility to start a bounded number of new processes. We prove that the defined Pathway Analysis captures all the properties of the systems, i.e. is precise. The results of the Pathway Analysis can be therefore used as an intermediate representation format, which is more concise than the Labelled Transition System with all the states explicitly represented and more suitable for devising efficient verification algorithms of concurrent systems than their process algebraic descriptions - see, for example, the reachability algorithm in Skrypnyuk and Nielson (2011) [17].