dc.contributor.author | Tristan, Jean-Baptiste F. | |
dc.contributor.author | Govereau, Paul | |
dc.contributor.author | Morrisett, John Gregory | |
dc.date.accessioned | 2011-03-22T20:23:43Z | |
dc.date.issued | 2011-03-22 | |
dc.identifier.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. | en_US |
dc.identifier.uri | http://nrs.harvard.edu/urn-3:HUL.InstRepos:4762396 | |
dc.description.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. | en_US |
dc.description.sponsorship | Engineering and Applied Sciences | en_US |
dc.language.iso | en_US | en_US |
dash.license | LAA | |
dc.subject | algorithms | en_US |
dc.subject | languages | en_US |
dc.subject | reliability | en_US |
dc.subject | theory | en_US |
dc.subject | verification | en_US |
dc.subject | translation validation | en_US |
dc.subject | symbolic evaluation | en_US |
dc.subject | LLVM | en_US |
dc.subject | optimization | en_US |
dc.subject | semantics of programming languages | en_US |
dc.subject | algebraic approaches to semantics | en_US |
dc.subject | logics and meanings of programs | en_US |
dc.subject | specifying and verifying and reasoning about programs | en_US |
dc.subject | mechanical verification | en_US |
dc.subject | studies of program constructs | en_US |
dc.subject | program and recursion schemes | en_US |
dc.title | Evaluating Value-Graph Translation Validation for LLVM | en_US |
dc.type | Conference Paper | en_US |
dc.description.version | Accepted Manuscript | en_US |
dash.depositing.author | Tristan, Jean-Baptiste F. | |
dc.date.available | 2011-03-22T20:23:43Z | |
dash.contributor.affiliated | Tristan, Jean-Baptiste F. | |
dash.contributor.affiliated | Govereau, Paul | |
dash.contributor.affiliated | Morrisett, Greg Gregory | |