A new technique is presented to statically check a given procedure against a user-provided property. The method requires no annotations; it automatically infers a context-dependent specification for each procedure call, so that only as much information about a procedure is used as is needed to analyze its caller. Specifications are inferred iteratively. Empty specifications are initially used to over-approximate the effects of all procedure calls; these are later refined in response to spurious counterexamples. When the analysis terminates, any remaining counterexample is guaranteed to be valid. However, since the heap is finitized, the absence of a counterexample does not guarantee the validity of the given property.
Inferring Specifications to Detect Errors in Code
Mana Taghdiri, Daniel Jackson
Journal of Automated Software Engineering (JASE)– Special issue on selected papers, Volume 14, Issue 1, 2007. (A preliminary version published in ASE’04.)