Abstract <p>Algebraic data types make it possible to represent complex data structures; therefore, the classical verification methods relying on inductive invariant inference are not applicable to programs with such types. The main difficulty in the classical methods is the weakness of the first-order logic language used to represent inductive invariants. In this paper, synchronous tree automata are considered as an alternative to the classical representations of invariants using first-order logic. A method for automatic inductive invariant inference represented by synchronous tree automata is proposed. This method uses finite-model findings. The implementation of the proposed method finds 65% more invariants than a first-order logic based tool, and it is a multiple winner of international verifier competition using inductive invariant inference.</p>