• CONCURRENCY—PRACTICE AND EXPER...

Treffer: CONCURRENCY—PRACTICE AND EXPERIENCE Concurrency: Pract. Exper. 2001; 13:1 Prepared using cpeauth.cls [Version: 2000/05/12 v2.0] Verified lightweight bytecode verification

Title:
CONCURRENCY—PRACTICE AND EXPERIENCE Concurrency: Pract. Exper. 2001; 13:1 Prepared using cpeauth.cls [Version: 2000/05/12 v2.0] Verified lightweight bytecode verification
Authors:
Gerwin Klein, Tobias Nipkow, Technische Universität München
Contributors:
The Pennsylvania State University CiteSeerX Archives
Source:
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ccpe01.pdf.
Collection:
CiteSeerX
Subject Terms:
KEY WORDS, Java, Bytecode Verification, Theorem Proving, Data Flow Analysis
Document Type:
Fachzeitschrift text
File Description:
application/pdf
Language:
English
Relation:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.2887
Availability:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.2887
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ccpe01.pdf
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.197D8108
Database:
BASE

Weitere Informationen

Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one-pass verification of welltypedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness.