Game semantics is a denotational semantics which constructs models of terms (open programs) by looking at the ways in which a term can observably interact with its environment. The obtained models are fully abstract (sound and complete), and are the most accurate models we can find for a programming language. Game semantics models can be given certain kinds of concrete automata-theoretic representations for several interesting language fragments with finite data types, and so they can serve as a basis for software model checking and program analysis. Here we examine several techniques for automatic verification of safety properties of terms with infinite data types. We have developed an abstraction-refinement procedure, which starts by model-checking the most abstract version of the concrete program. If no counterexample or a genuine one is found, the procedure terminates. Otherwise, it uses a spurious counterexample to gradually refine the abstraction for the next iteration. We can combine this approach with a method for verifying data-independent terms. We say that a term is data-independent with respect to a data type X, if the only operation available on values of type X is the equality test. We provide results which reduce the verification of some properties for all interpretations of X, to the verification for finite interpretations of X. Finally, we present a new symbolic approach for representing game semantics models, and show how it can be applied for efficient verification of terms. By using symbolic values instead of concrete ones, we generalize the standard notion of automata representation of game semantics to that of symbolic-automata representation. In this way terms with infinite data types can be expressed as finite-state symbolic-automata, and so various properties can be checked over them.