Improved analysis and refinement of integrated circuit device design and other programs is facilitated by methods in which an original program is partitioned into subprograms representing valid computational paths; each subprogram is refined when cyclic dependencies are found to exist between the variables; computational paths whose over-approximated reachable states are found to be contained in another computational path are merged; and finally, the remaining subprograms conjoined decision conditions become candidates for hints for program refinement.