Completeness of a bytecode verifier and a certifying Java-to-JVM compiler

DOI10.1023/A:1025003423108MaRDI QIDQ1405990zbMATH OpenOpenAlexFDO

Authors Robert F. Stärk, Joachim Schmid

Publication date 9 September 2003

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1025003423108

zbMATH Keywords

Javabytecode verificationcertifying compilation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Verified bytecode verification and type-certifying compilation
• scientific article; zbMATH DE number 1701360
• Verified bytecode verifiers.
• scientific article; zbMATH DE number 1796120
• A type system for the Java bytecode language and verifier

Cited in

(4)

• Fundamental Approaches to Software Engineering
• A certified lightweight non-interference Java bytecode verifier
• Verified bytecode verification and type-certifying compilation
• Preservation of Proof Obligations from Java to the Java Virtual Machine

This page was built for publication: Completeness of a bytecode verifier and a certifying Java-to-JVM compiler

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1405990)