LEADER 01784nam  2200373z- 450 
001 9910346893103321
005 20231214133634.0
010   $a1000028867
035   $a(CKB)4920000000101591
035   $a(oapen)https://directory.doabooks.org/handle/20.500.12854/52521
035   $a(EXLCZ)994920000000101591
100   $a20202102d2012      |y             0
101 0 $aeng
135   $aurmn|---annan
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 10$aA Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
210   $cKIT Scientific Publishing$d2012
215   $a1 electronic resource (XXI, 412 p. p.)
311   $a3-86644-885-6 
330   $aThe 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.
517   $aMachine-Checked, Type-Safe Model of Java Concurrency
517   $aA Machine-Checked, Type-Safe Model of Java Concurrency
610   $aJava
610   $aformal semantics
610   $atype safety
610   $amemory model
610   $aconcurrency
700   $aLochbihler$b Andreas$4auth$01312138
906   $aBOOK
912   $a9910346893103321
996   $aA Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler$93030734
997   $aUNINA