Conference Papers: Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler

Charakteristisch für die Programmiersprache Java sind sowohl ihre Sicherheitsgarantien wie beispielsweise Typsicherheit und die Sicherheitsarchitektur als auch die direkte Unterstützung von Threads. In der hier vorgestellten Dissertation wird ein maschinengeprüftes Modell von nebenläufigem Java einschließlich des Java-Speichermodells entwickelt und die Auswirkungen der Nebenläufigkeit auf diese Garantien untersucht. Aus dem formalen Modell wurde automatisch ein ausführbarer Interpreter, Übersetzer und eine virtuelle Maschine einschließlich eines Bytecode-Verifizierers generiert, mit dem das Modell empirisch gegen Java-Benchmarks validiert wurde.