Abstract-Refine is a relatively effective method in the field of software model checking

which has the advantages of high generality and efficiency. However

there is no framework for precise description and effective modular use or replacement of this method so far. This paper introduces a modular Abstract-Refine algorithm framework which analyzes and explains the structure of input program in fine-grained level. Also

this method modularly decouples Abstract-Refine algorithm from its sub-algorithms with the balancing operator

so that any modifications on sub-algorithms will not affect the upper level. Experiments verify that our approach can effectively implement modular decoupling of traditional algorithms

and will not impact the performance of original algorithms.