Sciweavers

Share
PLDI
2011
ACM

Evaluating value-graph translation validation for LLVM

9 years 14 days ago
Evaluating value-graph translation validation for LLVM
Translation validators are static analyzers that attempt to verify that program transformations preserve semantics. Normalizing translation 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 benchmarks that include GCC, a perl interpreter, SQLite3, and other C programs. Categories and Subject Descriptors F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages - Algebraic approaches to semantics; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - Mechanical Verification; F.3.3 [Logics and Meanings of Programs]: Stu...
Jean-Baptiste Tristan, Paul Govereau, Greg Morrise
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where PLDI
Authors Jean-Baptiste Tristan, Paul Govereau, Greg Morrisett
Comments (0)
books