Generating precise and concise procedure summaries

We present a framework for generating procedure summaries that are precise -- applying the summary in a given context yields the same result as re-analyzing the procedure in that context, and concise -- the summary exploits the commonalities in the ways edure manipulates abstract values, and does not contain superfluous context information. The use of a precise and concise procedure summary in modular analyses provides a way to capture infinitely many possible contexts in a finite way; in interprocedural analyses, it provides a compact representation of an explicit input-output summary table without loss of precision. e a class of abstract domains and transformers for which precise and concise summaries can be efficiently generated using our framework. Our framework is rich enough to encode a wide range of problems, including all IFDS and IDE problems. In addition, we show how the framework is instantiated to provide novel solutions to two hard problems: modular linear constant propag...

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Greta Yorsh, Eran Yahav, Satish Chandra
• Keywords: Linear Constant Propagation, POPL 2008, Programming Languages, Programs General Terms, Superfluous Context Information