Generating precise and concise procedure summaries

Abstract

We present a framework for generating procedure summaries that are (a) precise - applying the summary in a given context yields the same result as re-analyzing the procedure in that context, and(b) concise - the summary exploits the commonalitiesin the ways the procedure manipulates abstract values, and does not contain superfluous context information.