An effort to formalize the process of software pipelining loops with conditions is presented in this paper. A formal framework for scheduling such loops, based on representing sets of paths by matrices of predicates, has been proposed. Usual set operations and relationships may then be applied to such matrices. Operations of a loop body are placed into a single schedule with the flow of control implicitly encoded in predicate matrices. An algorithm that generates loop code from such an encoded schedule has been described. The framework is supported by a concrete proposed technique that iteratively parallelize loops, as well as with heuristics driven by data dependencies to efficiently shorten loop execution. Preliminary experimental results of our prototype implementation prove that the proposed framework, technique, and heuristics produce efficient code at acceptable cost.