Verified compilation in micro-Gypsy

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verified compilation in micro-Gypsy

Full text

Pdf (692 KB)

Source

International Symposium on Software Testing and Analysis archive
Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification table of contents

Key West, Florida, United States

Pages: 20 - 26

Year of Publication: 1989

ISBN:0-89791-342-6

Also published in ...

Author

W. Young

Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX

Sponsors

IEEE-CS : Computer Society
SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

ACM New York, NY, USA

Bibliometrics

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

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/75308.75312 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	Raymond Aubin, Mechanizing structural induction (formal system), 1976
	2	P. Baker, G. Dinolt, I. Freeman, M. Krenzin, R. Neely. Al Assurance for an Internet System: Doing the Job. Proceedings of the 9th National Computer Security Conference, September, 1986.
	3	W.R. Bevier. Kit: A Study in Operating System Verification. Tech Rept. CLI-28, CLInc, August, 1988.
	4	W. R. Bevier. A Formal Specification for a Core MIPS Machine. Tech. Rept. 29, Computational Logic, Inc., 1717 W. Sixth St., Suite 290, Austin, Texas 78703.1989.
	5	William R. Bevier , Warren A. Hunt, Jr. , J. Strother Moore , William D. Young, An approach to systems verification, Journal of Automated Reasoning, v.5 n.4, p.411-428, Dec. 1989
	6	W.R. Bevier, W.A. Hunt, W.D. Young. Toward Verified Execution Environments. Proceedings of the 1987 Symposium on Security and Privacy, IEEE, 1987.
	7	W.E. Boebert, W.D. Young, R.Y. Kain, S.A. Hansohn. Secure ADA Target: Issues, System Design, and Verification. Proceedings of the IEEE Symposium on Security and Privacy, 1985.
	8	R.S. Boyer, J S. Moore. A Computational Logic. Academic Press, New York, 1979.
	9	Robert S. Boyer , J. Strother Moore, A computational logic handbook, Academic Press Professional, Inc., San Diego, CA, 1988
	10	R.M. Burstall. "Proving Properties of Programs by Structural Induction". Computer Journal 12.1 (February 1969). 41-48.
	11	Robert Staley Cartwright, Jr., A practical formal semantic definition and verification system for typed lisp., 1977
	12	Laurian M. Chirica , David F. Martin, An approach to compiler correctness, Proceedings of the international conference on Reliable software, p.96-103, April 21-23, 1975, Los Angeles, California
	13	A. Cohn. Machine Assisted Proofs of Recursion Implementation. Ph.D. Th., University of Edinburgh, Edinburgh, Scotland, 1979.
	14	Dan Craigen. A Description of m-Verdi (Draft). Tech. Rept. 87-5420-02, I.P. Sharp Associates, Limited, Ottawa, Ontario, Canada, July, 1987.
	15	Department of Defense. Trusted Computer Systems Evafuation Criteria. DOD 5200.28-STD. December, 1985.
	16	James,H. Fetzer, Program verification: the very idea, Communications of the ACM, v.31 n.9, p.1048-1063, Sept. 1988 [doi>10.1145/48529.48530]
	17	D. Goldschilag. A Mechanically Verified Proof System for Concurrent Programs. Tech. Rept. 32, Computational Logic, Inc., 1717 W. Sixth St., Suite 290, Austin Texas 78703, 1989.
	18	D.I. Good. SCOMP Trusted Processes. ICSCA Internal Note 138, The University of Texas at Austin.
	19	D.I. Good, R.L. Akers, L.M. Smith. Report on Gypsy 2.05. Tech. Rept. CLI-1, CLInc, October, 1986.
	20	D.I. Good, R.L. Akers, L.M. Smith, and W.D. Young. Report on Micro-Gypsy (Draft). Tech. Rept. CLI-34, CLInc, November, 1988.
	21	D.I. Good, R.L. Akers, L.M. Smith, and W.D. Young. Report on Middle-Gypsy (Draft). Tech. Rept. CLI-35, CLInc, November, 1988.
	22	D.I. Good, B.L. Divito, M.K. Smith. Using The Gypsy Methodology. Tech. Rept. Draft CLI-2, CLInc, January, 1988.
	23	W. Henhapl and C.B. Jones. The Block Structure Concept and Some Possible Implementations. Tech. Rept. 25.104, IBM Laboratories, Vienna, 1970.
	24	Warren A. Hunt. FM8501: A Verified Microprocessor. Tech. Rept. ICSCA-CMP-47, Institute for Computing Science, University of Texas at Austin, December, 1985.
	25	W.A. Hunt. The Mechanical Verification of a Microprocessor Design. Tech. Rept. CLI-6, CLInc, September, 1986.
	26	P. Lucas. Two Constructive Realizations of the Block Concept and Their Realization. Tech. Rept. 25.082, IBM Laboratories, Vienna, 1968.
	27	D.S. Lynn. Interactive Compiler Proving Using Hoare Proof Rules. Tech. Rept. ISI/RR-78-70, Information Sciences Institute, January, 1978.
	28	John McCarthy. Towards a Mathematical Science of Computation. Proceedings of the IFIP Congress, Amsterdam, 1962.
	29	John McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. Proceeding of Symposium on Applied Mathematics, American Mathematical Society, 1967.
	30	R. Milner and R. Weyhrauch. Proving Compiler Correctness in a Mechanized Logic. In Machine Intelligence 7, Edinburgh University Press, Edinburgh, Scotland, 1972, pp. 5 l-70.
	31	Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
	32	J S. Moore. PITON: A Verified Assembly Level Language. Tech. Rept. CLI-22, CLInc, June, 1988.
	33	J S. Moore. A Mechanically Verified Language Implementation. Tech. Rept. CL130, CLInc, September, 1988.
	34	Wolfgang Polak, Compiler Specification and Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 1981
	35	A.E. Siebert and D.I. Good. General Message Flow Modulator. Tech. Rept. ICSCA-CMP-42, Institute for Computing Science, University of Texas at Austin, March, 1984.
	36	Michael K. Smith , Ann E. Siebert , Benedetto L. DiVito , Donald I. Good, A verified encrypted packet interface, ACM SIGSOFT Software Engineering Notes, v.6 n.3, p.13-16, July 1981 [doi>10.1145/1010832.1010838]
	37	W.D. Young. A Verified Code Generator for a Subset of Gypsy. Tech. Rept. CLI-33, CLInc. November, 1988.
	38	W.D. Young. A Verified Optimizer for Pica-Piton. Tech. Rept. Internal Note 107, CLInc. December, 1988.
	39	W.D. Young, J. McHugh. Coding for a Believable Specification to Implementation Mapping. Proceedings of the 1987 Symposium on Security and Privacy, IEEE, 1987.

CITED BY 2

	Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003
	Bishop C. Brock , Warren A. Hunt, Jr., The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor, Formal Methods in System Design, v.11 n.1, p.71-104, July 1997