Redundant proofs of non-interference in Levin-Gries CSP program proofs

DOI10.1007/BF00264361MaRDI QIDQ1077917zbMATH OpenOpenAlexFDO

Authors Thomas P. Murtagh

Publication date 1987

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00264361

zbMATH Keywords

non-interferenceproof system for Hoare's CSP languagesynchronization points

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

• Proving concurrent noninterference
• A proof system for abstract non-interference
• Computer Science Logic
• scientific article; zbMATH DE number 3903944
• Decidability and proof systems for language-based noninterference relations

This page was built for publication: Redundant proofs of non-interference in Levin-Gries CSP program proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1077917)