Static analysis by abstract interpretation is one of the widely used automatic approaches to program verification, due to its soundness guarantee and scalability. A key challenge for abstract interpretation with convex and linear abstract domain is verifying complex programs with disjunctive or non-linear behaviors. We propose to conduct abstract interpretation in an iterative forward and backward manner by utilizing dynamic input space partitioning to split the input space into sub-spaces such that each sub-space involves fewer disjunctive and non-linear program behaviors. We have implemented our approach, and the experimental results are promising.