Modular bug detection with inertial refinement

1. A method to detect an error in software with a computer readable code, comprising:

applying a modular analysis based on a structural abstraction and refinement of a program structure;

detecting an assertion violation indicative of a software bug;

performing inertial refinement of one or more program regions to avoid exploring a new region until necessary; and

employing one or more minimal correcting sets produced by a constraint solver to select one or more program regions to explore.

2. The method of claim 1 , comprising eapanding arbitray program regions during refinement Based on a hierarchical programm structure.

3. The method of claim 1 , comprising expanding a relevant placeholder and reducing the number of expanded placeholders.

4. The method of claim 1 , comprising employing blocking and unblocking paths to program regions using a path summary variable for a predetermined region.

5. The method of claim 1 , comprising expanding one or more loops dynamically during analysis.

6. The method of claim 1 , comprising expanding one or more recursive functions dynamically during analysis.

7. The method of claim 1 , comprising determining a local function summary using a side-effect analysis of a called function.

8. The method of claim 1 , wherein the modular analysis comprises an under-approximate data flow analysis, comprising:

a. approximating function summaries using structural abstraction;

b. checking error conditions using structural refinement; and

c. performing forward composition of summaries using a work list.

9. A system to detect errors in software, comprising:

a processor to execute the software;

computer readable code executable by the processor for applying a modular analysis of the software based on a structural abstraction and refinement of a program structure;

computer readable code executable by the processor for detecting an assertion violation indicative of a software bug;

computer readable code executable by the processor for performing inertial refinement of one or more program regions to avoid exploring a new region until necessary; and

computer readable code executable by the processor for employing one or more minimal correcting sets produced by a constraint solver to select one or more program regions to explore.

10. The system of claim 9 , comprising computer readable code executable by the processor for expanding arbitrary program regions during refinement based on a hierarchical program structure.

11. The system of claim 9 , comprising computer readable code executable by the processor for expanding a relevant placeholder and reducing the number of expanded placeholders.

12. The system of claim 9 , comprising computer readable code executable by the processor for employing blocking and unblocking paths to program regions using a path summary variable for a predetermined region.

13. The system of claim 9 , comprising computer readable code executable by the processor for expanding one or more loops dynamically during analysis.

14. The system of claim 9 , comprising computer readable code executable by the processor for expanding one or more recursive functions dynamically during analysis.

15. The system of claim 9 , comprising computer readable code executable by the processor for determining a local function summary using a side-effect analysis of a called function.

16. The system of claim 9 , wherein the modular analysis comprises an under-approximate data flow analysis, comprising:

a. computer readable code executable by the processor for approximating function summaries using structural abstraction;

b. computer readable code executable by the processor for checking error conditions using structural refinement; and

c. computer readable code executable by the processor for performing forward composition of summaries using a work list.