×

Using dynamic analysis to improve model checking

  • US 7,962,901 B2
  • Filed: 04/17/2006
  • Issued: 06/14/2011
  • Est. Priority Date: 04/17/2006
  • Status: Expired due to Fees
First Claim
Patent Images

1. A computerized method comprising:

  • instrumenting a program under test with code that records pointer dereference information;

    executing the instrumented program comprising recording pointer dereference frequency information;

    generating a Boolean program from the program under test; and

    exploring a model based at least on the Boolean program comprising using the pointer dereference frequency information and a points-to graph to direct state space exploration of the model for locating one or more bugs in the program under test;

    wherein exploring the model of the program further comprises exploring the model in an iteration that limits the points-to graph to at least one highest frequency memory location using the pointer dereference frequency information, then again exploring the model in one or more subsequent iterations until memory locations with corresponding pointer dereference frequency information are explored or until at least a bug is reported, wherein a subsequent iteration explores the model directed in part by limiting the points-to graph to a combination of at least one lower dereference frequency memory location and higher frequency memory locations of a preceding iteration.

View all claims
  • 2 Assignments
Timeline View
Assignment View
    ×
    ×