Most symbolic bug detection techniques perform search over the program
control flow graph based on either forward symbolic execution or backward
weakest preconditions computation. The complexity of determining interprocedural
all-path feasibility makes it difficult for such analysis to judge upfront
whether the behavior of a particular caller or callee procedure is relevant to
a given property violation. Consequently, these methods analyze several program
fragments irrelevant to the property, often repeatedly, before arriving at a goal location
or an entrypoint, thus wasting resources and diminishing their scalability.
This paper presents a systematic and scalable technique for focused bug detection
which, starting from the goal function, employs alternating backward and forward
exploration on the program call graph to lazily infer a small scope of program
fragments, sufficient to detect the bug or show its absence. The method learns
caller and callee invariants for procedures from failed exploration attempts and
uses them to direct future exploration towards a scope pertinent to the violation.
By: Nishant Sinha, Nimit Singhania, Satish Chandra, Manu Sridharan
Published in: RI12003 in 2012
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .