EVA STAR Trefferanzeige

Volltext 978-3-86644-885-8_pdfa.pdf1.pdf (5,4 MB)
Bestellung Die Veröffentlichung ist bei KIT Scientific Publishing erschienen.
Weitere Informationen sowie gegebenenfalls Bestellmöglichkeiten finden Sie hier.
DOI (für Zitat) http://dx.doi.org/10.5445/KSP/1000028867
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:0072-288672
Titel A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler
Autor Lochbihler, Andreas
Institution Institut für Programmstrukturen und Datenorganisation (IPD)
Dokumenttyp Buch
Verlag KIT Scientific Publishing, Karlsruhe
Jahr 2012
ISBN 978-3-86644-885-8
Hochschulschrift Dissertation
Fakultät für Informatik (INFORMATIK)
Institut für Programmstrukturen und Datenorganisation (IPD)
Prüfungsdaten: 12.07.2012
Referent/Betreuer: Prof. G. Snelting
Abstract 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.