Article

Free access

Verified compilation in micro-Gypsy

Author:

W. YoungAuthors Info & Claims

TAV3: Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification

Pages 20 - 26

https://doi.org/10.1145/75308.75312

Published: 01 November 1989 Publication History

PDF eReader

References

[1]

R. Aubin. Mechanizing Structural Induction. Ph.D. Th., University of Edinburgh, Edinburgh, Scotland, 1976.

Digital Library

Google Scholar

[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.

Google Scholar

[3]

W.R. Bevier. Kit: A Study in Operating System Verification. Tech Rept. CLI-28, CLInc, August, 1988.

Google Scholar

[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.

Google Scholar

[5]

W.R. Bevier, W.A. Hunt, Jr., J S. Moore, W.D. Young. An Approach to Systems Verification. to appear in Journal of Automated Reasoning, November, 1989.

Digital Library

Google Scholar

[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.

Crossref

Google Scholar

[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.

Crossref

Google Scholar

[8]

R.S. Boyer, J S. Moore. A Computational Logic. Academic Press, New York, 1979.

Google Scholar

[9]

R. S. Boyer and J S. Moore. A Computational Logic Handbook, Academic Press, Boston, 1988.

Digital Library

Google Scholar

[10]

R.M. Burstall. "Proving Properties of Programs by Structural Induction". Computer Journal 12.1 (February 1969). 41-48.

Crossref

Google Scholar

[11]

R. Cartwright. A Practical Formal Semantic Definition and Verfication System for Typed LISP. Ph.D. Th., Stanford University, 1976.

Digital Library

Google Scholar

[12]

L.M. Chirica and D.F. Martin. An Approach to Compiler Correctness. Proceedings of the International Conference on Reliable Software, April, 1975, pp. 96-103.

Digital Library

Google Scholar

[13]

A. Cohn. Machine Assisted Proofs of Recursion Implementation. Ph.D. Th., University of Edinburgh, Edinburgh, Scotland, 1979.

Google Scholar

[14]

Dan Craigen. A Description of m-Verdi (Draft). Tech. Rept. 87-5420-02, I.P. Sharp Associates, Limited, Ottawa, Ontario, Canada, July, 1987.

Google Scholar

[15]

Department of Defense. Trusted Computer Systems Evafuation Criteria. DOD 5200.28-STD. December, 1985.

Google Scholar

[16]

James H. Fetzer. "Program Verification: the Very Idea". Comm. of theACM31.9 (September 1988). 1048-1063.

Digital Library

Google Scholar

[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.

Google Scholar

[18]

D.I. Good. SCOMP Trusted Processes. ICSCA Internal Note 138, The University of Texas at Austin.

Google Scholar

[19]

D.I. Good, R.L. Akers, L.M. Smith. Report on Gypsy 2.05. Tech. Rept. CLI-1, CLInc, October, 1986.

Google Scholar

[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.

Google Scholar

[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.

Google Scholar

[22]

D.I. Good, B.L. Divito, M.K. Smith. Using The Gypsy Methodology. Tech. Rept. Draft CLI-2, CLInc, January, 1988.

Google Scholar

[23]

W. Henhapl and C.B. Jones. The Block Structure Concept and Some Possible Implementations. Tech. Rept. 25.104, IBM Laboratories, Vienna, 1970.

Google Scholar

[24]

Warren A. Hunt. FM8501: A Verified Microprocessor. Tech. Rept. ICSCA-CMP-47, Institute for Computing Science, University of Texas at Austin, December, 1985.

Google Scholar

[25]

W.A. Hunt. The Mechanical Verification of a Microprocessor Design. Tech. Rept. CLI-6, CLInc, September, 1986.

Google Scholar

[26]

P. Lucas. Two Constructive Realizations of the Block Concept and Their Realization. Tech. Rept. 25.082, IBM Laboratories, Vienna, 1968.

Google Scholar

[27]

D.S. Lynn. Interactive Compiler Proving Using Hoare Proof Rules. Tech. Rept. ISI/RR-78-70, Information Sciences Institute, January, 1978.

Google Scholar

[28]

John McCarthy. Towards a Mathematical Science of Computation. Proceedings of the IFIP Congress, Amsterdam, 1962.

Google Scholar

[29]

John McCarthy and J. Painter. Correctness of a Compiler for Arithmetic Expressions. Proceeding of Symposium on Applied Mathematics, American Mathematical Society, 1967.

Crossref

Google Scholar

[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.

Google Scholar

[31]

R. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976.

Digital Library

Google Scholar

[32]

J S. Moore. PITON: A Verified Assembly Level Language. Tech. Rept. CLI-22, CLInc, June, 1988.

Google Scholar

[33]

J S. Moore. A Mechanically Verified Language Implementation. Tech. Rept. CL130, CLInc, September, 1988.

Google Scholar

[34]

W. Polak. Compiler Specification and Verification. Springer-Verlag, Berlin, 1981.

Digital Library

Google Scholar

[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.

Google Scholar

[36]

M.K. Smith, A. Siebert, B. Divito, and D. Good. "A Verified Encrypted Packet Interface". Sojfware Engineering Notes 6,3 (July 1981).

Digital Library

Google Scholar

[37]

W.D. Young. A Verified Code Generator for a Subset of Gypsy. Tech. Rept. CLI-33, CLInc. November, 1988.

Google Scholar

[38]

W.D. Young. A Verified Optimizer for Pica-Piton. Tech. Rept. Internal Note 107, CLInc. December, 1988.

Google Scholar

[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.

Crossref

Google Scholar

Cited By

View all

Buck LYoung MBodenheimer B(2018)A Comparison of Distance Estimation in HMD-Based Virtual Environments with Different HMD-Based ConditionsACM Transactions on Applied Perception10.1145/319688515:3(1-15)Online publication date: 7-Jul-2018
https://dl.acm.org/doi/10.1145/3196885
Hopfgartner FHanbury AMüller HKando NMercer SKalpathy-Cramer JPotthast MGollub TKrithara ALin JBalog KEggel I(2015)Report on the Evaluation-as-a-Service (EaaS) Expert WorkshopACM SIGIR Forum10.1145/2795403.279541649:1(57-65)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2795403.2795416
Alonso OKamps JKarlgren J(2015)Report on the Seventh Workshop on Exploiting Semantic Annotations in Information Retrieval (ESAIR'14)ACM SIGIR Forum10.1145/2795403.279541249:1(27-34)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2795403.2795412
Show More Cited By

Index Terms

Recommendations

Verified compilation on a verified processor
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Developing technology for building verified stacks, i.e., computer systems with comprehensive proofs of correctness, is one way the science of programming languages furthers the computing discipline. While there have been successful projects verifying ...
From Verified Compilation to Secure Compilation: a Semantic Approach
PLAS'20: Proceedings of the 15th Workshop on Programming Languages and Analysis for Security

A formally verified compiler is a compiler that comes with a machine-checked proof that no bug is introduced during compilation. This correctness property states that the compiler preserves the semantics of programs. Formally verified compilers ...
Adapting Verified Compilation for Target-Language Errors

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

TAV3: Proceedings of the ACM SIGSOFT '89 third symposium on Software testing, analysis, and verification

November 1989

229 pages

ISBN:0897913426

DOI:10.1145/75308

Editor:
Richard A. Kemmerer

ACM SIGSOFT Software Engineering Notes Volume 14, Issue 8
Dec. 1989
213 pages
ISSN:0163-5948
DOI:10.1145/75309
Editor:
Richard N. Taylor
Univ. of California, Irvine
Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 1989

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

TAV-3

Sponsor:

SIGSOFT
IEEE-CS

TAV-3: 3rd Workshop on Software Testing Verification & Analysis

December 13 - 15, 1989

Florida, Key West, USA

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
544
Total Downloads

Downloads (Last 12 months)145
Downloads (Last 6 weeks)17

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Buck LYoung MBodenheimer B(2018)A Comparison of Distance Estimation in HMD-Based Virtual Environments with Different HMD-Based ConditionsACM Transactions on Applied Perception10.1145/319688515:3(1-15)Online publication date: 7-Jul-2018
https://dl.acm.org/doi/10.1145/3196885
Hopfgartner FHanbury AMüller HKando NMercer SKalpathy-Cramer JPotthast MGollub TKrithara ALin JBalog KEggel I(2015)Report on the Evaluation-as-a-Service (EaaS) Expert WorkshopACM SIGIR Forum10.1145/2795403.279541649:1(57-65)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2795403.2795416
Alonso OKamps JKarlgren J(2015)Report on the Seventh Workshop on Exploiting Semantic Annotations in Information Retrieval (ESAIR'14)ACM SIGIR Forum10.1145/2795403.279541249:1(27-34)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2795403.2795412
Zhai CCohen WLafferty J(2015)Beyond Independent RelevanceACM SIGIR Forum10.1145/2795403.279540549:1(2-9)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2795403.2795405
Repenning AWebb DKoh KNickerson HMiller SBrand CHorses IBasawapatna AGluck FGrover RGutierrez KRepenning N(2015)Scalable Game DesignACM Transactions on Computing Education10.1145/270051715:2(1-31)Online publication date: 30-Apr-2015
https://dl.acm.org/doi/10.1145/2700517
Bodden ETolêdo TRibeiro MBrabrand CBorba PMezini M(2013)SPLLIFTACM SIGPLAN Notices10.1145/2499370.249197648:6(355-364)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2491976
Cohen NPetrank E(2013)Limitations of partial compactionACM SIGPLAN Notices10.1145/2499370.249197348:6(309-320)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2491973
Sankaranarayanan SChakarov AGulwani S(2013)Static analysis for probabilistic programsACM SIGPLAN Notices10.1145/2499370.246217948:6(447-458)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462179
Guha AReitblatt MFoster N(2013)Machine-verified network controllersACM SIGPLAN Notices10.1145/2499370.246217848:6(483-494)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2462178
Guha AReitblatt MFoster NBoehm HFlanagan C(2013)Machine-verified network controllersProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2462178(483-494)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2462178
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Verified compilation on a verified processor

From Verified Compilation to Secure Compilation: a Semantic Approach

Adapting Verified Compilation for Target-Language Errors