Show simple item record

dc.contributor.author
Rauch, Nicole
dc.contributor.author
Wolff, Burkhart
dc.date.accessioned
2017-08-14T07:21:41Z
dc.date.available
2017-06-10T19:31:19Z
dc.date.available
2017-08-14T07:21:41Z
dc.date.issued
2004
dc.identifier.uri
http://hdl.handle.net/20.500.11850/69782
dc.identifier.doi
10.3929/ethz-a-006775190
dc.description.abstract
We present a formal model of the Java two’s-complement integral arithmetics. The model directly formalizes the arithmetic 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.
en_US
dc.language.iso
en
en_US
dc.publisher
ETH, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
SPECIAL PROGRAMMING METHODS
en_US
dc.subject
SPEZIELLE PROGRAMMIERMETHODEN
en_US
dc.subject
JAVA (PROGRAMMING LANGUAGES)
en_US
dc.subject
JAVA (PROGRAMMIERSPRACHEN)
en_US
dc.title
Formalizing Java’s Two’s-Complement Integral Type in Isabelle/HOL
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
ethz.journal.title
ETH technical report
ethz.journal.volume
458
en_US
ethz.size
144 p.
en_US
ethz.code.ddc
0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.notes
Technical Reports D-INFK.
en_US
ethz.identifier.nebis
006775190
ethz.publication.place
Zurich
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
ethz.date.deposited
2017-06-10T19:34:36Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59366b14e988372382
ethz.identifier.importid
imp593650d3791dd69960
ethz.ecolpid
eth:4791
ethz.ecitpid
pub:110489
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-16T01:54:34Z
ethz.rosetta.lastUpdated
2017-08-14T07:21:57Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Formalizing%20Java%E2%80%99s%20Two%E2%80%99s-Complement%20Integral%20Type%20in%20Isabelle/HOL&rft.jtitle=ETH%20technical%20report&rft.date=2004&rft.volume=458&rft.au=Rauch,%20Nicole&Wolff,%20Burkhart&rft.genre=report&
 Search via SFX

Files in this item

Thumbnail

Publication type

Show simple item record