An axiomatic semantics for nested concurrency

We give transformation rules for the concurrent parts of Hoare's language CSP, transforming concurrent CSP programs into nondeterministic, sequential programs.On the basis of these transformations we define an axiomatic semantics for CSP with nested concurrency.This axiomatic system includes a rule for binary, associative process composition, enabling modular verification dealing with parts of concurrent systems as well as full programs.The proof system is fully abstract, in the sense that the internal structure of processes is irrelevant in the specification inasmuch it is not externally observable.An outline of a verification of a recursive, concurrent sorter is given as an example.