Apt (1986) Correctness proofs of distributed termination algorithms. ACM Trans. Programming Languages Syst. 8:388-405.
Back (1988) A calculus of refinements for program derivations. Acta Inform. 25:593-624.
Back (1989) A method for refining atomicity in parallel algorithms. Lecture Notes in Computer Science , Springer, Berlin; 366:199-216.
Back, Kurki-Suonio (1983) Decentralization of process nets with centralized control. Proceedings 2nd ACM Symposium on Principles of Distributed Computing 131-142.
Back, Kurki-Suonio (1988) Distributed cooperation with action systems. ACM Trans. Programming Languages Syst. 10:513-554.
Best (1979) A note on the proof of a concurrent program. Inform. Process. Lett. 9:103-104.
Chandy, Misra (1986) An example of stepwise refinement of distributed programs: Quiescence detection. ACM Trans. Programming Languages Syst. 8:326-343.
Chandy, Misra Parallel Program Design: A Foundation, Addison-Wesley, Reading, MA; 1988.
Clarke (1977) Program invariants as fixed points. Proceedings 18th IEEE Symposium on Foundations of Computer Science 18-29.
Clarke (1980) Synthesis of resource invariants for concurrent programs. ACM Transactions on Programming Languages and Systems 2:338-358.
Clarke, Grumberg, Browne (1986) Reasoning about networks with many identical finite-state processes. Proceedings 5th ACM Symposium on Principles of Distributed Computing 240-248.
Cousot, Cousot (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings 4th ACM Symposium on Principles of Programming Languages 238-252.
Cousot, Cousot (1989) A language independent proof of the soundness and completeness of generalized Hoare logic. Inform. Comput. 80:165-191.
Cousot, Halbwachs (1978) Automatic discovery of linear restraints among variables of a program. Proceedings 5th ACM Symposium on Principles of Programming Languages 84-96.
de Bakker, Meertens (1975) On the completeness of the inductive assertion method. J. Comput. Syst. Sci. 11:323-357.
de Bakker Mathematical Theory of Program Correctness, Prentice-Hall, Englewood Cliffs, NJ; 1980.
Dijkstra A Discipline of Programming, Prentice-Hall, Englewood Cliffs, NJ; 1976.
Dijkstra (1977) A correctness proof for networks of communicating processes: A small exercise. EWD 607, Burroughs, Netherlands; .
Dijkstra (1978) On-the-fly garbage collection: An exercise in cooperation. Comm. ACM 21:966-975.
Dijkstra (1979) Finding the correctness proof of a concurrent program. Lecture Notes in Computer Science , Springer, Berlin; 69:24-34.
Dijkstra (1979) On the Interplay between Mathematics and Programming. Lecture Notes in Computer Science , Springer, Berlin; 69:35-46.
Gerth (1984) Transition logic. Proceedings 16th ACM Symposium on Theory of Computing 39-50.
Keller (1976) Formal verification of parallel programs. Comm. ACM 19:371-384.
Lamport (1980) The “Hoare logic” of concurrent programs. Acta Inform. 14:21-37.
Lamport (1983) An assertional correctness proof of a distributed algorithm. Science of Computer Programming 2:175-206.
Lamport, Schneider (1984) The “Hoare logic” of CSP. ACM Transactions on Programming Languages and Systems , and all that; 6:281-296.
Lamport (1987) win and sin: Predicate transformers for concurrency. DEC SRC Rept. 17.
Lamport (1988) Control predicates are better than dummy variables for reasoning about program control. ACM Trans. Programming Languages Syst. 10:267-281.
Lamport (1988) A theorem on atomicity in distributed algorithms. DEC SRC Rept. 28.
Lipton (1975) Reduction: A method of proving properties of parallel programs. Comm. ACM 18:717-721.
Lynch, Tuttle (1987) Hierarchical correctness proofs for distributed algorithms. Proceedings 6th ACM Symposium on Principles of Distributed Computing 137-151.
Morgan (1988) The specification statement. ACM Trans. Programming Languages Syst. 10:403-419.
Morgan (1988) Auxiliary variables in data refinement. Inform. Process. Lett. 29:293-296.
Morris (1987) A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Programming 9:287-306.
Morris (1987) Varieties of weakest liberal preconditions. Inform. Process. Lett. 25:207-210.
Owicki, Gries (1976) An axiomatic proof technique for parallel programs. Acta Inform. 6:319-340.
Raynal Algorithms for Mutual Exclusion, North Oxford Academic; 1986.
Sifakis (1982) A unified approach for studying the properties of transition systems. Theoret. Comput. Sci. 18:227-259.
van Lamsweerde, Sintzoff (1979) Formal derivation of strongly correct concurrent programs. Acta Inform. 12:1-31.
Wolper, Lovinfosse (1989) Verifying properties of large sets of processes with network invariants. Proceedings Workshop on Automatic Verifivation, Grenoble, France; .
