Using dynamic analysis to improve model checking
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.
2 Assignments
0 Petitions
Accused Products
Abstract
Model checking has been used to verify program behavior. However, exploration of the model is often impractical for many general purpose programs due to the complexity of an exploding state space. Instead, a program is instrumented with code that records pointer dereference information. The instrumented program is executed thereby recording pointer dereference frequency information. Then, a model of the program is explored using the pointer dereference frequency information to direct state space exploration of the model.
-
Citations
18 Claims
-
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 Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15)
-
-
16. A computer system comprising:
-
a digital processor; and digital memory comprising, a program under test, an abstractor generating a Boolean program using the program under test as input, and a binary instrumentor instrumenting the program under test to provide pointer dereference frequency information, and a model checker for exploring a model built based at least on the Boolean program using the pointer dereference frequency information and a points-to graph to focus a state space exploration for locating one or more bugs in the program under test, wherein the exploring the model comprises focusing the exploration of 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 using a combination of at least one lower frequency memory location and higher frequency memory locations of a preceding iteration.
-
-
17. A computer-readable storage medium having computer-executable instructions that when executed cause a computer to perform a method, the 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 constructed 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 in order to locate one or more bugs in the program under test; wherein exploring the model of the program further comprises exploring the model in a first 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 one bug is reported, wherein a subsequent iteration limits the points-to graph to a combination of at least one lower frequency memory location and higher frequency memory locations of a preceding iteration. - View Dependent Claims (18)
-
Specification