A Report On The Development Of Gypsy

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A Report On The Development Of Gypsy

Full text

Pdf (814 KB)

Source

ACM Annual Conference/Annual Meeting archive
Proceedings of the 1978 annual conference table of contents

Washington, D.C., United States

Pages: 116 - 122

Year of Publication: 1978

ISBN:0-89791-000-1

Authors

Donald I. Good
Richard M. Cohen
Lawrence W. Hunter

Sponsor

ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 13, Citation Count: 0

Additional Information:

abstract references 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/800127.804078 What is a DOI?

ABSTRACT

The first version of Gypsy was introduced in 1976 to support the specification and construction of verified programs. A second version has evolved based on the experiences of the last two years. The changes introduced in the second version are described. Some experiences with the specification and proof methodology are discussed, and the status of the implementation of the Gypsy compiler and verification system is summarized.

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	A. Ambler, D.I. Good, W.F. Burger. "Report on the Language Gypsy", The University of Texas at Austin, ICSCA-CMP-1 August, 1976.
	2	Per Brinch Hansen. Operating Systems Principles, Prentice-Hall, 1973.
	3	Per Brinch Hansen, The purpose of concurrent Pascal, Proceedings of the international conference on Reliable software, p.305-309, April 21-23, 1975, Los Angeles, California
	4	D.I. Good, ed. "Constructing Verifiably Reliable and Secure Communications Processing Systems", Final Report of the Certifiable Minicomputer Project, ICSCA-CMP-6, The University of Texas at Austin, 1977.
	5	Donald I. Good, Constructing verified and reliable communications processing systems, ACM SIGSOFT Software Engineering Notes, v.2 n.5, p.8-13, October 1977 [doi>10.1145/1005882.1005885]
	6	D.I. Good, R.M. Cohen, C.G. Hoch, L.W. Hunter, D.F. Hare. "Report on the Language Gypsy: Version 2.0", Certifiable Minicomputer Project, ICSCA-CMP-10, The University of Texas at Austin, 1978.
	7	D.I. Good and R.M. Cohen. "Verifiable Communications Processing in Gypsy", in Proceedings of Compcon, '78, September, 1978.
	8	Donald I. Good , Richard M. Cohen , James Keeton-Williams, Principles of proving concurrent programs in Gypsy, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.42-52, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567757]
	9	John B. Goodenough, Exception handling: issues and a proposed notation, Communications of the ACM, v.18 n.12, p.683-696, Dec. 1975 [doi>10.1145/361227.361230]
	10	C.A.R. Hoare. "Proof of Correctness of Data Representations", In Acta Informatica, 4, 1972.
	11	C.A.R. Hoare and N. Wirth. "An Axiomatic Definition of the Programming Language PASCAL", In Acta Informatica 2, 1973.
	12	C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
	13	Charles George Hoch, Hardware support for modern software concepts., 1978
	14	Gary R. Horn. "Specifications for a Secure Computer Communications Network", Master's Thesis, The University of Texas at Austin, 1977.
	15	John H. Howard, Proving monitors, Communications of the ACM, v.19 n.5, p.273-279, May 1976 [doi>10.1145/360051.360079]
	16	Shigeru Igarashi , Ralph L. London , David C. Luckham, Automatic program verification I: a logical basis and its implementation., Stanford University, Stanford, CA, 1973
	17	Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
	18	Anita K. Jones , Barbara H. Liskov, A language extension for expressing constraints on data access, Communications of the ACM, v.21 n.5, p.358-367, May 1978 [doi>10.1145/359488.359493]
	19	B. Liskov and S. Zilles. "An Approach to Abstraction", In Computation Structures Group Memo 88, MIT, 1973.
	20	Mark Steven Moriconi, A system for incrementally designing and verifying programs., 1977
	21	P.G. Neumann, L. Robinson, K.N. Levitt, R.S. Boyer, A.R. Saxena. "A Provably Secure Operating System", SRI Project 2581, prepared for USAECOM, June, 1975.
	22	D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
	23	Larry Calvin Ragland, A verified program-verifier., 1973
	24	O. Roubine and L. Robinson. "SPECIAL Reference Manual", Stanford Research Institute, August, 1976.
	25	B.J. Walker. "Verification of the UCLA Security Kernel: Data Defined Specifications", Master's Thesis, University of California at Los Angeles, 1977.
	26	R.E. Wells. "Specification and Implementation of a Verifiable Communications System", Master's Thesis, The University of Texas at Austin, December, 1976.