About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
POPL 1982
Conference paper
Modular verification of concurrent programs
Abstract
Verifying concurrent systems can be difficult because of the complex interactions possible between system components. In this paper, we propose a technique to simplify the task: modular composition of sequential proofs. We model a parallel program as a set of modules that interact by procedure calls. The properties of each module are proved using a sequential-program verification technique. If the modules satisfy a set of constraints presented in this paper, we may compose the modules into a system and the properties of the modules into properties of the system. The constraints ensure that the specifications are robust for each module where they are defined or used, in the sense that they are unaffected by current actions of other modules. A specification can be guaranteed robust for module m by restricting it to local variables of m, or by using monotonic predicates, which once true remain true forever. Our technique can be used to prove safety and liveness properties of parallel programs-the liveness properties are specified using temporal logic.