Show simple item record

dc.contributor.authorKlein, Gerwin
dc.contributor.editorWagner, Dorothea
dc.date.accessioned2017-09-22T20:42:05Z
dc.date.available2017-09-22T20:42:05Z
dc.date.issued2004
dc.identifier.isbn978-3-88579-408-X
dc.identifier.issn1617-5468
dc.identifier.urihttp://dl.gi.de/handle/20.500.12116/4471
dc.description.abstractDer Bytecode Verifier ist ein essenzieller Bestandteil der Sicherheitsarchitektur der Programmierplattform Java. Meine Dissertation stellt eine formale, ausführbare Spezifikation des Bytecode Verifiers vor sowie den Beweis, dass diese korrekt ist. Die Formalisierung, vollständig im Theorembeweiser Isabelle durchgeführt, besteht aus einem abstrakten Framework für Bytecode-Verifikation, das mit zunehmend ausdrucksstarken Typsystemen instanziiert wird. Diese decken sämtliche wichtigen Eigenschaften der Java-Plattform ab. Die Formalisierung liefert zwei ausführbare, verifizierte Bytecode Verifier: den Standard-Algorithmus, wie er auf normalen Desktop- Rechnern benutzt wird, sowie einen Lightweight Bytecode Verifier für eingebettete Systeme mit Ressourcenbeschränkungen wie z.B. Java SmartCards.de
dc.language.isode
dc.publisherGesellschaft für Informatik
dc.relation.ispartofAusgezeichnete Informatikdissertationen 2003
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Dissertations, Volume D-4
dc.titleVerified Java Bytecode Verificationde
dc.pubPlaceBonn
mci.reference.pages91-100


Files in this item

Thumbnail

Show simple item record