Redundant proofs of non-interference in Levin-Gries CSP program proofs (Q1077917)

The proof system for Hoare's CSP language proposed by Levin and Gries requires that non-interference be proven for each assertion used in the proof of a process. In the worst case, the effort required to provide such proofs could be enormous. The need for these proofs has been identified as a significant weakness of the system. In this paper, we show that most of the proofs of non-interference required are unnecessary. In particular, we show that once proofs of non-interference have been found for those assertions that precede certain synchronization points in a program the remaining proofs of non-interference required in the Levin-Gries system can be constructed automatically. This suggests that proving non-interference in the Levin-Gries system may be far less burdensome than had previously been assumed.