We first introduce a calculus for handling ground integer arithmetic
in first-order logic. The method is tailored to Java program
verification and meant to be used both as a supporting procedure and
simplifier during interactive verification and as an automated tool
for discharging (ground) proof obligations. It is fully implemented as
part of the KeY verification system. There are four main components: a
complete procedure for linear equations, a complete procedure for
linear inequalities, an incomplete procedure for nonlinear
(polynomial) equations, and an incomplete procedure for nonlinear
inequalities. The calculus is complete for the generation of
counterexamples for invalid ground formulas in integer arithmetic.

As work in progress, we then discuss how the calculus can be extended
to deal with quantifiers. The proposed approach is based on the work
by Martin Giese on tableaux with incremental closure. In the theory of
linear integer arithmetic, this naturally leads to a formulation of
the Omega test. Incomplete procedures are obtained for more expressive
fragments like nonlinear (polynomial) integer arithmetic or arithmetic
together with uninterpreted function symbols.