The ``Hoare Logic'' of CSP, and All That

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The ``Hoare Logic'' of CSP, and All That

Full text

Pdf (918 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 6 , Issue 2 (April 1984) table of contents

Pages: 281 - 296

Year of Publication: 1984

ISSN:0164-0925

Authors

Leslie Lamport	Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA
Fred B. Schneider	Department of Computer Science, Cornell University, Ithaca, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 6, Downloads (12 Months): 75, Citation Count: 17

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/2993.357247 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
	2	ASHCROFT, E.A. Proving assertions about parallel programs. J. Comput. Syst. Sci. 10 (Jan. 1975), 110-135.
	3	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
	4	COUSOT, P., AND COUSOT, R. Reasoning about program invariance proof methods. Tech. Rep. CRIN-80-P0, Centre de Recherche en Informatique de Nancy, Nancy, France, July 1980.
	5	Patrick Cousot , Radhia Cousot, Semantic Analysis of Communicating Sequential Processes (Shortened Version), Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.119-133, July 14-18, 1980
	6	COUSOT, P., AND COUSOT, R. On the soundness and completeness of generalized Hoare logic. Tech. Rep. CRIN-80-P093. Centre de Recherche en Informatique de Nancy, Nancy, France, Dec. 1982.
	7	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	8	FLOYD, R.W. Assigning Meanings to Programs. In Proceedings of the Symposium on Applied Mathematics, vol. 19. American Mathematical Society, Providence, R.I., 1967, pp. 19-32.
	9	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	10	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	11	Robert M. Keller, Formal verification of parallel programs, Communications of the ACM, v.19 n.7, p.371-384, July 1976 [doi>10.1145/360248.360251]
	12	LAMPORT, L. Proving correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Mar. 1977), 125-143.
	13	LAMPORT, L. The 'Hoare Logic' of concurrent programs. Acta inf. 14 (1980), 21-37.
	14	Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
	15	LEVIN, G.M., AND GRIES, D. A proof technique for communicating sequential processes. Acta in{. 15 ( 1981), 281-302.
	16	Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
	17	Susan Speer Owicki, Axiomatic proof techniques for parallel programs., 1975
	18	OWICKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs. Acta In{. 6 (1976), 319-340.
	19	SCHLICHTING, R.D., AND SCHNEIDER, F.B. Using message passing for distributed programming: Proof rules and disciplines. Tech. Rep., Dep. of Computer Science, Cornell Univ., Ithaca, N.Y.

CITED BY 17

	Joylyn Reed , Raymond T. Yeh, Specification and verification of liveness properties of cyclic, concurrent processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.1, p.156-177, Jan. 1988
	Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989
	Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993
	Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
	Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada
	Laura K. Dillon, Using symbolic execution for verification of Ada tasking programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.4, p.643-669, Oct. 1990
	Leslie Lamport, win and sin: predicate transformers for concurrency, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.396-428, July 1990
	Richard D. Schlichting , Fred B. Schneider, Using message passing for distributed programming: proof rules and disciplines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.402-431, July 1984
	David K. Probst , Hon F. Li, Abstract pecification of Synchronous Data Types for VLSI and Proving the Correctness of Systolic Network Implementations, IEEE Transactions on Computers, v.37 n.6, p.710-720, June 1988
	Jennifer L. Welch , Leslie Lamport , Nancy Lynch, A lattice-structured proof of a minimum spanning, Proceedings of the seventh annual ACM Symposium on Principles of distributed computing, p.28-43, August 15-17, 1988, Toronto, Ontario, Canada
	Leslie Lamport, Control predicates are better than dummy variables for reasoning about program control, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.267-281, April 1988
	Leslie Lamport, Reasoning about nonatomic operations, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.28-37, January 24-26, 1983, Austin, Texas
	Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Wim H. Hesselink, Wait-free linearization with an assertional proof, Distributed Computing, v.8 n.2, p.65-80, October 1994
	Leslie Lamport , Fred B. Schneider, Constraints: a uniform approach to aliasing and typing, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.205-216, January 14-16, 1985, New Orleans, Louisiana, United States
	Long Li , Yu Zhang , Yi-Yun Chen , Yong Li, Certifying concurrent programs using transactional memory, Journal of Computer Science and Technology, v.24 n.1, p.110-121, January 2009