METHOD FOR OPTIMIZING INTEGRATED CIRCUIT DEVICE DESIGN AND SERVICE

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.