The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.02 - March (1977 vol.3)
pp: 125-143
L. Lamport , Massachusetts Computer Associates, Inc.
ABSTRACT
The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.
INDEX TERMS
synchronization, Assertions, concufrent programming, correctness, multiprocessing
CITATION
L. Lamport, "Proving the Correctness of Multiprocess Programs", IEEE Transactions on Software Engineering, vol.3, no. 2, pp. 125-143, March 1977, doi:10.1109/TSE.1977.229904
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool