Verified lightweight bytecode verification

Gerwin Klein; Tobias Nipkow

doi:10.1002/cpe.597

Verified lightweight bytecode verification

Gerwin Klein, Tobias Nipkow

Informatik 7 - Lehrstuhl für Theoretische Informatik

Technische Universität München

Publikation: Beitrag in Fachzeitschrift › Artikel › Begutachtung

23 Zitate (Scopus)

Abstract

An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.

Originalsprache	Englisch
Seiten (von - bis)	1133-1151
Seitenumfang	19
Fachzeitschrift	Concurrency and Computation: Practice and Experience
Jahrgang	13
Ausgabenummer	13
DOIs	https://doi.org/10.1002/cpe.597
Publikationsstatus	Veröffentlicht - Nov. 2001

Zugriff auf Dokument

10.1002/cpe.597

Andere Dateien und Links

Verknüpfung zur Publikation in Scopus

Dieses zitieren

@article{fcd2efa385a44b5d9bd2014eceb0de2a,

title = "Verified lightweight bytecode verification",

abstract = "An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.",

keywords = "Bytecode verification, Data flow analysis, Java, Theorem proving",

author = "Gerwin Klein and Tobias Nipkow",

year = "2001",

month = nov,

doi = "10.1002/cpe.597",

language = "English",

volume = "13",

pages = "1133--1151",

journal = "Concurrency and Computation: Practice and Experience",

issn = "1532-0626",

publisher = "John Wiley and Sons Ltd",

number = "13",

}

TY - JOUR

T1 - Verified lightweight bytecode verification

AU - Klein, Gerwin

AU - Nipkow, Tobias

PY - 2001/11

Y1 - 2001/11

N2 - An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.

AB - An annotation of java virtual machine code with types to enable a one-pass verification of well-typedness was proposed. It contains the lightweight bytecode verifier as an executable functional program. The lightweight bytecode verifier builds on the existing specification of the whole μJava language.

KW - Bytecode verification

KW - Data flow analysis

KW - Java

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=0035506225&partnerID=8YFLogxK

U2 - 10.1002/cpe.597

DO - 10.1002/cpe.597

M3 - Article

AN - SCOPUS:0035506225

SN - 1532-0626

VL - 13

SP - 1133

EP - 1151

JO - Concurrency and Computation: Practice and Experience

JF - Concurrency and Computation: Practice and Experience

IS - 13

ER -

Verified lightweight bytecode verification

Abstract

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren