A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler (Record no. 78338)

MARC details
000 -LEADER
fixed length control field 01679naaaa2200301uu 4500
001 - CONTROL NUMBER
control field https://directory.doabooks.org/handle/20.500.12854/52521
005 - DATE AND TIME OF LATEST TRANSACTION
control field 20220220092115.0
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number KSP/1000028867
020 ## - INTERNATIONAL STANDARD BOOK NUMBER
International Standard Book Number 9783866448858
024 7# - OTHER STANDARD IDENTIFIER
Standard number or code 10.5445/KSP/1000028867
Terms of availability doi
041 0# - LANGUAGE CODE
Language code of text/sound track or separate title English
042 ## - AUTHENTICATION CODE
Authentication code dc
100 1# - MAIN ENTRY--PERSONAL NAME
Personal name Lochbihler, Andreas
Relationship auth
245 10 - TITLE STATEMENT
Title A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
260 ## - PUBLICATION, DISTRIBUTION, ETC.
Name of publisher, distributor, etc. KIT Scientific Publishing
Date of publication, distribution, etc. 2012
300 ## - PHYSICAL DESCRIPTION
Extent 1 electronic resource (XXI, 412 p. p.)
506 0# - RESTRICTIONS ON ACCESS NOTE
Terms governing access Open Access
Source of term star
Standardized terminology for access restriction Unrestricted online access
520 ## - SUMMARY, ETC.
Summary, etc. The Java programming language provides safety and security guarantees such as type safety and its security architecture. They distinguish it from other mainstream programming languages like C and C++. In this work, we develop a machine-checked model of concurrent Java and the Java memory model and investigate the impact of concurrency on these guarantees. From the formal model, we automatically obtain an executable verified compiler to bytecode and a validated virtual machine.
540 ## - TERMS GOVERNING USE AND REPRODUCTION NOTE
Terms governing use and reproduction Creative Commons
Use and reproduction rights https://creativecommons.org/licenses/by-nc-nd/4.0/
Source of term cc
-- https://creativecommons.org/licenses/by-nc-nd/4.0/
546 ## - LANGUAGE NOTE
Language note English
653 ## - INDEX TERM--UNCONTROLLED
Uncontrolled term Java
653 ## - INDEX TERM--UNCONTROLLED
Uncontrolled term formal semantics
653 ## - INDEX TERM--UNCONTROLLED
Uncontrolled term type safety
653 ## - INDEX TERM--UNCONTROLLED
Uncontrolled term memory model
653 ## - INDEX TERM--UNCONTROLLED
Uncontrolled term concurrency
856 40 - ELECTRONIC LOCATION AND ACCESS
Host name www.oapen.org
Uniform Resource Identifier <a href="https://www.ksp.kit.edu/9783866448858">https://www.ksp.kit.edu/9783866448858</a>
Access status 0
Public note DOAB: download the publication
856 40 - ELECTRONIC LOCATION AND ACCESS
Host name www.oapen.org
Uniform Resource Identifier <a href="https://directory.doabooks.org/handle/20.500.12854/52521">https://directory.doabooks.org/handle/20.500.12854/52521</a>
Access status 0
Public note DOAB: description of the publication

No items available.