This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Proving the Correctness of Multiprocess Programs
March 1977 (vol. 3 no. 2)
pp. 125-143
L. Lamport, Massachusetts Computer Associates, Inc.
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
Usage of this product signifies your acceptance of the Terms of Use.