Integer Arithmetic in the Specification and Verification of Java Programs

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert und Steffen Schlager
In:Workshop on Tools for System Design and Verification (FM-TOOLS 2002)
Jahr:2002
Seiten:7-14

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.

BibTeX

@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}
}