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.