Patent ID: 8522226

Claim:
A method for discovering a set of possible iterative sequences for a given loop in a program, comprising: partitioning the loop into a plurality of portions based on control flow in the loop, each of the plurality of portions representing multiple paths in the control flow; associating labels with the portions; constructing an initial loop automaton in memory storage that represents loop iterations as a regular language over the labels corresponding to the portions in the program; analyzing subsequences of the labels to determine infeasibility of the subsequences permitted in the automaton; and refining the loop automaton by removing all infeasible subsequences to discover a set of possible iteration sequences, wherein analyzing subsequences of the labels includes determining whether there is a proof of infeasibility in a current subsequence; and if proof exists, deriving invariants from the proof, and wherein partitioning the loop into a plurality of portions includes partitioning the loop using splitting criteria including one or more of outcome of branches in the loop, back edges traversed by an iteration, and induction variable updates.