Let $S$ be Spec $O_K$ with $O_K$ the ring of integers of a number field $K$.

Let $X\to S $ be an arithmetic variety, i.e., an integral smooth quasi-projective $S$-scheme with generic fibre $X_\eta$ geometrically connected.

Suppose that I highly suspect that $X\to O_K$ has no sections. Now, how could I prove that this is really the case? (This is equivalent to saying that $X_\eta$ has no integral points with respect to the model $X\to S$, I believe.)

Is there a "computable" necessary criterion $X\to S$ must satisfy for $X(S)$ to be non-empty? What about a sufficient criterion?

If $S$ is Spec $\mathbf{Q}$ one could try to check whether $X(\mathbf{Q}_v)$ is empty for example.