
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
19th Annual Symposium on Foundations of Computer Science (FOCS 1978)
Consistent and complete proof rules for the total correctness of parallel programs
October 16October 18
ASCII Text  x  
Lawrence Flon, Norihisa Suzuki, "Consistent and complete proof rules for the total correctness of parallel programs," 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, pp. 184192, 19th Annual Symposium on Foundations of Computer Science (FOCS 1978), 1978.  
BibTex  x  
@article{ 10.1109/SFCS.1978.11, author = {Lawrence Flon and Norihisa Suzuki}, title = {Consistent and complete proof rules for the total correctness of parallel programs}, journal ={2013 IEEE 54th Annual Symposium on Foundations of Computer Science}, volume = {0}, year = {1978}, issn = {02725428}, pages = {184192}, doi = {http://doi.ieeecomputersociety.org/10.1109/SFCS.1978.11}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  CONF JO  2013 IEEE 54th Annual Symposium on Foundations of Computer Science TI  Consistent and complete proof rules for the total correctness of parallel programs SN  02725428 SP184 EP192 A1  Lawrence Flon, A1  Norihisa Suzuki, PY  1978 VL  0 JA  2013 IEEE 54th Annual Symposium on Foundations of Computer Science ER   
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SFCS.1978.11
We describe a formal theory of the total correctness of parallel programs, including such heretofore theoretically incomplete properties as safety from deadlock and starvation. We present a consistent and complete set of proof rules for the total correctness of parallel programs expressed in nondeterministic form. The proof of consistency and completeness is novel in that we show that the weakest preconditions for each correctness criterion are actually fixedpoints (least or greatest) of continuous functions over the complete lattice of total predicates. We have obtained proof rule schemata which can universally be applied to least or greatest fixed points of continuous functions. Therefore, our proof rules are a priori consistent and complete once it is shown that certain weakest preconditions are extremum fixedpoints. The relationship between true parallelism and nondeterminism is also discussed.
Citation:
Lawrence Flon, Norihisa Suzuki, "Consistent and complete proof rules for the total correctness of parallel programs," focs, pp.184192, 19th Annual Symposium on Foundations of Computer Science (FOCS 1978), 1978
Usage of this product signifies your acceptance of the Terms of Use.