Data Independent Induction over Structured Networks.
Sadie Creese, Andrew William Roscoe · 2000
We extend the classes of network which Data Independent Induction can be used to reason about. Through the use of constants and predicates in the data independent type we build proofs of structured networks' behaviours, where a network's topology need not be as regular as one might expect data independence to imply. These properties hold true independent of the size of the type, and so for arbitrary network size. The inductions combine the use of the process algebra CSP to model systems and their specifications, and the FDR tool to discharge the various proof obligations.