@TechReport{ rauch.ea:formalizing:2004, abstract = {We present a formal model of Java two’s-complement integral arithmetics. The model directly formalizes the artihmetic operations as given in the Java Language Specification (JLS). The algebraic properties of these definitions are derived. Underspecifications and ambiguities in the JLS are pointed out and clarified. The theory is formally analyzed in Isabelle/HOL that is, machine-checked proofs for the ring properties and divisor/remainder theorems etc. are provided. This work is suited to build the framework for machine-supported reasoning over arithmetic formulae in the context of Java source-code verification. }, author = {Nicole Rauch and Burkhart Wolff}, institution = {ETH Z\"urich}, language = {USenglish}, month = 11, number = 458, pdf = {papers/2004/root.pdf}, title = {Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL}, year = 2004, user = {wolff} }