VOC: A translation validator for optimizing compilers

Lenore Zuck; Amir Pnueli; Yi Fang; Benjamin Goldberg

doi:10.1016/S1571-0661(04)80393-1

VOC: A translation validator for optimizing compilers

Lenore Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg

Computer Science

Research output: Contribution to journal › Conference article › peer-review

Abstract

The VOC, a methodology for translation validation of optimizing compilers, is discussed. VOC-64 is described as a tool which is developed to perform automatic translation validation for the SGI Pro/64 compiler, and gave examples of the VCs it generates. Structure preserving optimization are distinguished, for which a simulation relation is established between the source target code based on computational induction, and structure modifying optimizations. One of the main problems is the current need to interface with a 'heavy' package.

Original language	English (US)
Pages (from-to)	2-18
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	65
Issue number	2
DOIs	https://doi.org/10.1016/S1571-0661(04)80393-1
State	Published - Apr 2002
Event	COCV'02 Compiler Optimization Meets Compiler Verification (Satellite Event of ETAPS 2002) - Grenoble, France Duration: Apr 13 2002 → Apr 13 2002

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/S1571-0661(04)80393-1

Cite this

@article{3dce7dd50bca47f784a20d91f3002d41,

title = "VOC: A translation validator for optimizing compilers",

abstract = "The VOC, a methodology for translation validation of optimizing compilers, is discussed. VOC-64 is described as a tool which is developed to perform automatic translation validation for the SGI Pro/64 compiler, and gave examples of the VCs it generates. Structure preserving optimization are distinguished, for which a simulation relation is established between the source target code based on computational induction, and structure modifying optimizations. One of the main problems is the current need to interface with a 'heavy' package.",

author = "Lenore Zuck and Amir Pnueli and Yi Fang and Benjamin Goldberg",

note = "Copyright: Copyright 2018 Elsevier B.V., All rights reserved.; COCV'02 Compiler Optimization Meets Compiler Verification (Satellite Event of ETAPS 2002) ; Conference date: 13-04-2002 Through 13-04-2002",

year = "2002",

month = apr,

doi = "10.1016/S1571-0661(04)80393-1",

language = "English (US)",

volume = "65",

pages = "2--18",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "2",

}

TY - JOUR

T1 - VOC

T2 - COCV'02 Compiler Optimization Meets Compiler Verification (Satellite Event of ETAPS 2002)

AU - Zuck, Lenore

AU - Pnueli, Amir

AU - Fang, Yi

AU - Goldberg, Benjamin

PY - 2002/4

Y1 - 2002/4

N2 - The VOC, a methodology for translation validation of optimizing compilers, is discussed. VOC-64 is described as a tool which is developed to perform automatic translation validation for the SGI Pro/64 compiler, and gave examples of the VCs it generates. Structure preserving optimization are distinguished, for which a simulation relation is established between the source target code based on computational induction, and structure modifying optimizations. One of the main problems is the current need to interface with a 'heavy' package.

AB - The VOC, a methodology for translation validation of optimizing compilers, is discussed. VOC-64 is described as a tool which is developed to perform automatic translation validation for the SGI Pro/64 compiler, and gave examples of the VCs it generates. Structure preserving optimization are distinguished, for which a simulation relation is established between the source target code based on computational induction, and structure modifying optimizations. One of the main problems is the current need to interface with a 'heavy' package.

UR - http://www.scopus.com/inward/record.url?scp=1442358113&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=1442358113&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80393-1

DO - 10.1016/S1571-0661(04)80393-1

M3 - Conference article

AN - SCOPUS:1442358113

SN - 1571-0661

VL - 65

SP - 2

EP - 18

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

Y2 - 13 April 2002 through 13 April 2002

ER -

VOC: A translation validator for optimizing compilers

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this