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.



Detecting sections on an arithmetic variety
It sounds as if you are asking for an algorithm which, in particular, would be able to tell whether a given set of polynomials over $\mathbb{Z}$ admits an integer solution. This is [Hilbert's 10th problem](http://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem) and it is known that no such algorithm exists in general.


For specific classes of variety, it's certainly possible to look at necessary conditions from the local-global point of view: taking $S = \textbf{Spec}\;\mathbb{Z}$, a necessary condition for solubility is existence of $\mathbb{Z}\_p$-points for all $p$. Even for quadrics, this condition is known not to be sufficient, but one can define a Brauer-Manin obstruction: for a nice account of this, see Colliot-Thélène and Xu's article ["Brauer-Manin obstruction for integral points of homogeneous spaces and representation of integral quadratic forms"](http://www.math.u-psud.fr/~colliot/CTXuCompositio2009.pdf).


