BEGIN:VCALENDAR
PRODID:-//Mercury//HGEvent//EN
VERSION:2.0
METHOD:PUBLISH
BEGIN:VEVENT
STATUS:CONFIRMED
LAST-MODIFIED:20130524T031521
PRIORITY:0
CLASS:PUBLIC
UID:ATEvent-eed436ece7e23bbcfe0d4623c4969225
SUMMARY:Ph.D. Thesis Proposal: Cong Hou
DESCRIPTION:Ph.D. Thesis Proposal\nTitle: Synthesis for Program InversionCong HouSchool of Computational Science and EngineeringCollege of ComputingGeorgia Institute of TechnologyDate: October 8th (Monday)\, 2012Time: 1:00PM - 3:00PM (EDT)Location: KACB 1315Committee:\nDr. Richard Vuduc (Advisor\, School of Computational Science and Engineering\, Georgia Tech)Dr. Richard Fujimoto (School of Computational Science and Engineering\, Georgia Tech)Dr. Santosh Pande (School of Computer Science\,Georgia Tech)Dr. Daniel Quinlan (Lawrence Livermore National Laboratory)Dr. David Jefferson (Lawrence Livermore National Laboratory)Abstract:Program inversion has been successfully applied to several areas such as optimistic parallel discrete event simulation (OPDES) and reverse debugging. Given a program P with input state I and output state O\, its inverse or reverse program\, P-\, produces I given O. When P is not injective or reversible\, we need to build an instrumented and reversible version of P that we call a forward program and is denoted by P+\, so that it becomes possible to construct P- from P+. The instrumented code in P+ stores control flow information and values that cannot be recovered. However\, constructing forward and reverse programs manually is a tedious\, time-consuming\, and error-prone task. We need an automated tool that can generate forward and reverse programs automatically. In this thesis we introduce an automatic program inversion framework for imperative languages. In our method\, we transform the task of program inversion into a problem of retrieving values. Specifically\, we build a value search graph (VSG) that explicitly expresses equality relations between values in the program. Values in the graph are represented by single static assignment (SSA) names or constant values. Equalities are detected from assignments\, comparisons\, some special operations\, global value numbering\, etc.. Each equality is constrained by a set of control flow paths on which the equality exists. The problem of building forward and reverse programs then becomes a combinatorial search problem on the VSG. The forward and reverse programs are then generated based on the search result. Using the same framework\, we first describe how to retrieve scalar values\, then extend it to handling arrays and other data structures (e.g. object access and linked data structure). To handle arrays\, we introduce the array subregion representations into the VSG so that the equality between two arrays holds only in the subregion attached to it. Then we retrieve an array by retrieving subregions of it. We also show that object access and linked data structure can be transformed into array-like representations so that the same method will be employed to handle them.\n
DTSTART:20121008T130000
DTEND:20121008T150000
CREATED:20121220T171509
DTSTAMP:20121220T171509
SEQUENCE:0
LOCATION:
END:VEVENT
END:VCALENDAR