2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2004)
Sept. 20, 2004 to Sept. 24, 2004
Mana Taghdiri , Massachusetts Institute of Technology, Cambridge, MA
A new static program analysis method for checking structural properties of code is proposed. The user need only provide a property to check; no further annotations are required. An initial abstraction of the code is computed that over-approximates the effect of function calls. This abstraction is then iteratively refined in response to spurious counterexamples. The refinement involves inferring a context-dependent specification for each function call, so that only as much information about a function is used as is necessary to analyze its caller. When the algorithm terminates, the remaining counterexample is guaranteed not to be spurious, but because the program and its heap are finitized, absence of a counterexample does not constitute proof.
Mana Taghdiri, "Inferring Specifications to Detect Errors in Code", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 144-153, 2004, doi:10.1109/ASE.2004.10075