Using transformations to verify parallel programs

  • Ernst-Rüdiger Olderog
  • Krzysztof R. Apt
Part I Invited Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 490)


We argue that the verification of parallel programs can be considerably simplified by using program transformations. We illustrate this approach by proving correctness of two parallel programs under the assumption of fairness: asynchronous fixed point computation and parallel zero search.


Parallel Program Parallel Composition Proper State Fair Termination Program Transformation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E. Ashcroft and Z. Manna, Formalization of properties of parallel programs, Machine Intelligence 6, pp. 17–41, 1971.Google Scholar
  2. [2]
    K.R. Apt and E.-R. Olderog, Proof rules and transformations dealing with fairness, Science of Computer Programming 3, pp. 65–100, 1983.Google Scholar
  3. [3]
    R.J.R. Back, A method for refining atomicity in parallel algorithms, Lecture Notes in Computer Science 366, Springer-Verlag, 1989.Google Scholar
  4. [4]
    M. Chandy and J. Misra, A Foundation of Parallel Program Design, Addison-Wesley, 1988.Google Scholar
  5. [5]
    E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM 18, pp. 453–457, 1975.Google Scholar
  6. [6]
    L. Flon and N. Suzuki, The total correctness of parallel programs, SIAM Journal of Computing, pp. 227–246, 1978.Google Scholar
  7. [7]
    N. Francez, Fairness, Springer-Verlag, 1986.Google Scholar
  8. [8]
    M.C.B.Hennessy and G.D. Plotkin, Full abstraction for a simple programming language, Lecture Notes in Computer Science 74, Springer-Verlag, 1979.Google Scholar
  9. [9]
    L. Lamport, Proving the correctness of multiprocess programs, IEEE Transactions on Software Engineering SE-3:2, pp.125–143, 1977.Google Scholar
  10. [10]
    R. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM 18, pp. 717–721, 1975.Google Scholar
  11. [11]
    E. R. Olderog and K. R. Apt, Fairness in parallel programs, the transformational approach, ACM TOPLAS 10, pp. 420–455, 1988.Google Scholar
  12. [12]
    S. Owicki and D. Gries, An axiomatic proof technique for parallel programs, Acta Informatica 6, pp. 319–340, 1976.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Ernst-Rüdiger Olderog
    • 1
  • Krzysztof R. Apt
    • 2
    • 3
  1. 1.Department of Computer ScienceUniversity of OldenburgOldenburgFederal Republic of Germany
  2. 2.Centre for Mathematics and Computer ScienceAmsterdamThe Netherlands
  3. 3.Department of Computer SciencesUniversity of Texas at AustinAustinU.S.A.

Personalised recommendations