Show simple item record

dc.contributor.advisorMorrisett, John Gregory
dc.contributor.authorGovereau, Paul
dc.date.accessioned2013-01-02T18:42:39Z
dc.date.issued2013-01-02
dc.date.submitted2011
dc.identifier.citationGovereau, Paul. 2012. Denotational Translation Validation. Doctoral dissertation, Harvard University.en_US
dc.identifier.otherhttp://dissertations.umi.com/gsas.harvard:10045en
dc.identifier.urihttp://nrs.harvard.edu/urn-3:HUL.InstRepos:10121982
dc.description.abstractIn this dissertation we present a simple and scalable system for validating the correctness of low-level program transformations. Proving that program transformations are correct is crucial to the development of security critical software tools. We achieve a simple and scalable design by compiling sequential low-level programs to synchronous data-flow programs. Theses data-flow programs are a denotation of the original programs, representing all of the relevant aspects of the program semantics. We then check that the two denotations are equivalent, which implies that the program transformation is semantics preserving. Our denotations are computed by means of symbolic analysis. In order to achieve our design, we have extended symbolic analysis to arbitrary control-flow graphs. To this end, we have designed an intermediate language called Synchronous Value Graphs (SVG), which is capable of representing our denotations for arbitrary control-flow graphs, we have built an algorithm for computing SVG from normal assembly language, and we have given a formal model of SVG which allows us to simplify and compare denotations. Finally, we report on our experiments with LLVM M.D., a prototype denotational translation validator for the LLVM optimization framework.en_US
dc.description.sponsorshipEngineering and Applied Sciencesen_US
dc.language.isoen_USen_US
dash.licenseLAA
dc.subjectcompilationen_US
dc.subjectvalidationen_US
dc.subjectcomputer scienceen_US
dc.titleDenotational Translation Validationen_US
dc.typeThesis or Dissertationen_US
dc.date.available2013-01-02T18:42:39Z
thesis.degree.date2012en_US
thesis.degree.disciplineComputer Scienceen_US
thesis.degree.grantorHarvard Universityen_US
thesis.degree.leveldoctoralen_US
thesis.degree.namePh.D.en_US
dc.contributor.committeeMemberSmith, Michaelen_US
dc.contributor.committeeMemberChong, Stephenen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record