Publication: Evaluating Value-Graph Translation Validation for LLVM
Loading...
Open/View Files
Date
2011-03-22
Published Version
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
The Harvard community has made this article openly available. Please share how this access benefits you.
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.
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.
Description
Other Available Sources
Research Data
Keywords
algorithms, languages, reliability, theory, verification, translation validation, symbolic evaluation, LLVM, optimization, semantics of programming languages, algebraic approaches to semantics, logics and meanings of programs, specifying and verifying and reasoning about programs, mechanical verification, studies of program constructs, program and recursion schemes
Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material (LAA), as set forth at Terms of Service