Invariant generation is the automatic discovery of loop invariants — logical assertions that hold at the beginning of every loop iteration and are strong enough to prove a desired postcondition. Since loop invariants are the key human-supplied ingredient in deductive verification (Hoare logic, weakest precondition), automating their discovery is one of the central challenges in formal methods. Techniques include abstract interpretation (computing fixed points in abstract domains), template-based inference (positing invariant shapes and solving for coefficients), predicate abstraction (searching over Boolean combinations of candidate predicates), and machine learning approaches that learn invariant patterns from data.
In the verification workflow of Floyd-Hoare, the human provides loop invariants and the tool generates and checks verification conditions. Invariant generation aims to automate the human's job — discovering loop invariants automatically so that verification becomes fully push-button. This is one of the most active and impactful research areas in formal methods because the loop invariant is usually the only thing standing between a fully annotated program and a complete correctness proof.
Abstract interpretation is the most mature approach. The abstract interpretation framework computes loop invariants by iterating the abstract transfer function until convergence. Starting from the abstract initial state, the analysis applies the abstract loop body repeatedly, widening when necessary to force convergence. The resulting fixed point is an invariant: it holds on entry (by construction from the initial state), is preserved by the loop body (it is a fixed point of the transfer function), and its precision depends on the abstract domain. The interval domain produces invariants like "0 <= i AND i <= n"; the octagon domain produces "x - y <= 5 AND x + y <= 10"; the polyhedra domain produces arbitrary linear invariants. Each domain captures a different class of numerical relationships.
Template-based methods posit a parametric invariant shape and solve for the parameters. For example, assume the invariant has the form "a*x + b*y + c <= 0" and search for values of a, b, c that satisfy the initiation and consecution conditions. This reduces invariant generation to constraint solving (often via SMT or linear programming). The method is flexible — you can search for polynomial invariants, disjunctive invariants, or any shape you can template — but the choice of template is itself a design decision that limits what can be discovered.
Predicate abstraction generates Boolean invariants over a set of candidate predicates. Given predicates like "x > 0", "i < n", "arr[i] = old_arr[i]", the method searches for a Boolean combination (conjunction, disjunction) that serves as an invariant. When combined with CEGAR, new predicates are discovered from spurious counterexamples: if the current predicate set is too coarse, the counterexample reveals which new predicate would distinguish the conflated states. This approach, implemented in SLAM and BLAST, has been particularly successful for control-dominated programs (device drivers, protocols) where the relevant invariants are Boolean combinations of program conditions.
Recent work explores machine learning for invariant generation. Neural networks trained on (program, invariant) pairs learn patterns that generalize to new programs. The Code2Inv and LoopInvGen systems use reinforcement learning or neural-guided search to propose invariant candidates, which are then verified by SMT solvers. These approaches can discover invariants that fall outside the fixed templates of classical methods, though they currently lack the completeness guarantees of abstract interpretation. The frontier of the field is combining the generalization of learning with the soundness of formal verification — using ML to propose and formal methods to verify.