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.