Integer Arithmetic in the Specification and Verification of Java Programs

@InProceedings{BeckertSchlager2002,
  author =       {Bernhard Beckert and Steffen Schlager},
  title =        {Integer Arithmetic in the Specification and
		  Verification of {J}ava Programs},
  booktitle =    {Workshop on Tools for System Design and
		  Verification ({FM-TOOLS} 2002)},
  abstract =     {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.},
  venue =        {Reisensburg, Germany},
  pages =        {7--14},		  
  year =         {2002}
}