Alternate and Learn: Finding Witnesses without Looking All over

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 inter-procedural all-path feasibility makes it difficult for such analysis to judge up-front 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.