A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler

A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler

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 i...

Full description

Saved in:
Bibliographic Details
:
Lochbihler, Andreas
Year of Publication:2012
Language:English
Physical Description:1 electronic resource (XXI, 412 p. p.)
Tags: Add Tag
No Tags, Be the first to tag this record!
id 993545490504498
ctrlnum (CKB)4920000000101591
(oapen)https://directory.doabooks.org/handle/20.500.12854/52521
(EXLCZ)994920000000101591
collection bib_alma
record_format marc
spelling Lochbihler, Andreas auth
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
Machine-Checked, Type-Safe Model of Java Concurrency
A Machine-Checked, Type-Safe Model of Java Concurrency
KIT Scientific Publishing 2012
1 electronic resource (XXI, 412 p. p.)
text txt rdacontent
computer c rdamedia
online resource cr rdacarrier
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.
English
Java
formal semantics
type safety
memory model
concurrency
3-86644-885-6
language English
format eBook
author Lochbihler, Andreas
spellingShingle Lochbihler, Andreas
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
author_facet Lochbihler, Andreas
author_variant a l al
author_sort Lochbihler, Andreas
title A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_full A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_fullStr A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_full_unstemmed A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_auth A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_alt Machine-Checked, Type-Safe Model of Java Concurrency
A Machine-Checked, Type-Safe Model of Java Concurrency
title_new A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
title_sort a machine-checked, type-safe model of java concurrency : language, virtual machine, memory model, and verified compiler
publisher KIT Scientific Publishing
publishDate 2012
physical 1 electronic resource (XXI, 412 p. p.)
isbn 1000028867
3-86644-885-6
illustrated Not Illustrated
work_keys_str_mv AT lochbihlerandreas amachinecheckedtypesafemodelofjavaconcurrencylanguagevirtualmachinememorymodelandverifiedcompiler
AT lochbihlerandreas machinecheckedtypesafemodelofjavaconcurrency
AT lochbihlerandreas amachinecheckedtypesafemodelofjavaconcurrency
status_str n
ids_txt_mv (CKB)4920000000101591
(oapen)https://directory.doabooks.org/handle/20.500.12854/52521
(EXLCZ)994920000000101591
carrierType_str_mv cr
is_hierarchy_title A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
_version_ 1796649061619597313
fullrecord <?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>01619nam-a2200349z--4500</leader><controlfield tag="001">993545490504498</controlfield><controlfield tag="005">20231214133634.0</controlfield><controlfield tag="006">m o d </controlfield><controlfield tag="007">cr|mn|---annan</controlfield><controlfield tag="008">202102s2012 xx |||||o ||| 0|eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">1000028867</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)4920000000101591</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(oapen)https://directory.doabooks.org/handle/20.500.12854/52521</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)994920000000101591</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Lochbihler, Andreas</subfield><subfield code="4">auth</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler</subfield></datafield><datafield tag="246" ind1=" " ind2=" "><subfield code="a">Machine-Checked, Type-Safe Model of Java Concurrency</subfield></datafield><datafield tag="246" ind1=" " ind2=" "><subfield code="a">A Machine-Checked, Type-Safe Model of Java Concurrency</subfield></datafield><datafield tag="260" ind1=" " ind2=" "><subfield code="b">KIT Scientific Publishing</subfield><subfield code="c">2012</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 electronic resource (XXI, 412 p. p.)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">English</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Java</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">formal semantics</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">type safety</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">memory model</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">concurrency</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-86644-885-6</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2023-12-15 06:00:51 Europe/Vienna</subfield><subfield code="f">system</subfield><subfield code="c">marc21</subfield><subfield code="a">2019-11-10 04:18:40 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&amp;portfolio_pid=5337929710004498&amp;Force_direct=true</subfield><subfield code="Z">5337929710004498</subfield><subfield code="b">Available</subfield><subfield code="8">5337929710004498</subfield></datafield></record></collection>

Similar Items