Integer Arithmetic in the Specification and Verification of Java Programs Bernhard Beckert and Steffen Schlager In this paper we present an approach for handling integer arithmetic in the specification and verification of Java programs. In particular, problems like overflow and underflow arising from the finiteness of the Java types are tackled.