Program composition and modular verification

1. K.R. Apt, F.S. de Boer, E.-R. Olderog: “Proving termination of parallel programs,” in W. Feijen, N. van Gasteren, D. Gries, J. Misra (eds.): “Beauty is our business, a birth-day salute to Edsger W. Dijkstra,” Springer-Verlag, 1990. Also: TR CS-R9016, CWI Amsterdam May 1990.

   Google Scholar 

2. A.V. Aho, J.E. Hopcropf, J.D. Ullman: “The design and analysis of computer algorithms,” Addison-Wesley, 1974.

   Google Scholar 

3. K.R. Apt: “Formal justification of a proof system for communication sequential processes,” Journal of the ACM, vol. 30, No. 1, January 1983, pp. 197–216.

   Google Scholar 

4. L. Bouge, N. Francez: “A Compositional Approach to Superimposition,” 15th ACM Symp. on Principles of Programming Languages, San Diego, CA, January 1988.

   Google Scholar 

5. M. Chandy, J. Misra: “Parallel programs design,” Addison-Wesly, 1988.

   Google Scholar 

6. E.W. Dijkstra, W.H.J. Feijen, A.J.M. van Gasteren: “Derivation of a termination detection algorithm for distributed computations,” IPL 16, pp. 217–219, 1983.

   Google Scholar 

7. N. Francez, I.R. Forman: “Superimposition for interacting processes,” CONCUR'90, Amsterdam, August 1990. LNCS 458 J.C.M. Baeten, J.W. Klop (Eds.), Springer-Verlag, 1990.

   Google Scholar 

8. L. Fix, N. Francez, O. Grumberg: “Semantics-driven decompositions for the verification of distributed programs,” Proc. of the IFIP working group 2.2/2.3 working conference on Programming concepts and Methods, Sea of Galilee, Israel, April 1990, North-Holland, pp. 101–123.

   Google Scholar 

9. N. Francez: “Fairness,” Springer-Verlag, 1986.

   Google Scholar 

10. E. Gafni: “Perspectives on Distributed Network Protocols: A Case for Building Blocks,” MILCON 86, Monterey, Ca., October 1986.

    Google Scholar 

11. C.A.R. Hoare: “Communicating sequential processes,” CACM 21, 8, August 1978, pp. 666–677.

    Google Scholar 

12. S. Katz: “A Superimposition Control Construct for Distributed Systems”, submitted to Transaction on Programming Languages and Systems. Preliminary version MCC technical Report STP-268-87.

    Google Scholar 

13. J. Misra, M. Chandy: “Proofs of networks of processes,” IEEE SE 7(4), 1981.

    Google Scholar 

14. J. Misra: “Preserving progress under program composition,” Notes on UNITY: 17–20.

    Google Scholar 

15. S. Owicki, D. Gries: “An axiomatic proof technique for parallel programs,” Acta Informatica 6, 1976.

    Google Scholar 

16. S. Ramesh: “On the completeness of modular proof systems,” IPL 36, pp. 195–201, 1990.

    Google Scholar 

17. C. Stirling: “A generalization of Owicki-Gries's Hoare logic for a concurrent while language,” Theoretical computer science no. 58 pp. 347–359, 1988.

    Google Scholar 

18. J. Zwiers, W.P. de Roever, P. van Emde Boas: “Compositionality and concurrent networks: soundness and completeness of a proof system,” Proc. 12th ICALP, Nafplion, Greece, July 1985, Springer LNCS 194, pp. 509–519.

    Google Scholar 

19. J. Zwiers: “Compositionality, concurrency and partial correctness,” Springer LNCS 321, 1989.

    Google Scholar 

Download references