Evaluating Value-Graph Translation Validation for LLVM

DSpace/Manakin Repository

Evaluating Value-Graph Translation Validation for LLVM

Citable link to this page


Title: Evaluating Value-Graph Translation Validation for LLVM
Author: Tristan, Jean-Baptiste F.; Govereau, Paul; Morrisett, John Gregory

Note: Order does not necessarily reflect citation order of authors.

Citation: Tristan, Jean-Baptiste, Paul Govereau, and Greg Morrisett. Forthcoming. Evaluating value-graph translation validation for LLVM. Paper presented at ACM SIGPLAN Conference on Programming and Language Design Implementation, June 4-8, 2011, San Jose, California.
Full Text & Related Files:
Abstract: Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing trans- lation validators do so by trying to match the value-graphs of an original function and its transformed counterpart. In this paper, we present the design of such a validator for LLVM’s intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present the results of our preliminary experiments on a set of bench- marks that include GCC, a perl interpreter, SQLite3, and other C programs.
Terms of Use: This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:4762396
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search