Show simple item record

dc.contributor.authorJha, Somesh
dc.contributor.authorLu, Shan
dc.contributor.authorJin, Guoliang
dc.contributor.authorHarris, William R.
dc.description.abstractProgrammers who develop large, mature applications often want to optimize the performance of their program without changing the semantics of the program. They often do so by changing how their program invokes a library function or a function provided by another module of the program. Unfortunately, once a programmer makes such an optimization, it is difficult for him to determine that the optimization does not change the semantics of the original program, because the orig- inal and optimized programs are equivalent only due to subtle, implicit assumptions about library functions called by the programs. In this work, we present an interactive program analysis that a program- mer can apply to determine that his optimization does not change the behavior of a program. Our analysis casts the problem of validating an optimization as an abductive inference problem in the context of checking program equivalence. Our analysis solves the abductive equivalence prob- lem by interacting with the programmer so that the programmer imple- ments a solver for a logical theory that models library functions invoked by the program. We have used our analysis to validate optimizations from a set real-world, mature applications consisting of the Apache webserver, the Mozilla software suite, and the MySQL database.en
dc.subjectprogram optimizationen
dc.subjectprogram equivalenceen
dc.subjectabductive reasoningen
dc.titleValidating Library Usage Interactivelyen
dc.typeTechnical Reporten

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record