To solve the partial correct problem of loop program, an algorithm was presented to generate non-linear loop invariant by computing Dixon resultant based on algebraic transition system and constraint system. The loop program was firstly transformed to an algebraic transition system, then a polynomial set was constructed from algebraic transition relation and invariant template, and a constraint system w.r.t template variable was obtained by computing Dixon resultant. Finally the constraint system was resolved to get invariant. The algorithm was effective to whether single-path or multi-path programs through case study.
