Verified bytecode verification and type-certifying compilation

DOI10.1016/J.JLAP.2003.07.004MaRDI QIDQ1881665zbMATH OpenOpenAlexFDO

Authors Gerwin Klein, Martin Strecker

Publication date 14 October 2004

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2003.07.004

zbMATH Keywords

Bytecode verificationCompilerJavaJVMTheorem proving

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Recommendations

• scientific article; zbMATH DE number 1980940
• scientific article; zbMATH DE number 1701360
• Verified bytecode verifiers.
• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• A type system for the Java bytecode language and verifier

Cites work

• Java: Embedding a programming language in a theorem prover
• Hoare logic for Java in Isabelle/HOL
• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 1692947 (Why is no real title available?)
• scientific article; zbMATH DE number 1701360 (Why is no real title available?)
• scientific article; zbMATH DE number 986407 (Why is no real title available?)
• scientific article; zbMATH DE number 1231622 (Why is no real title available?)
• scientific article; zbMATH DE number 1956459 (Why is no real title available?)
• scientific article; zbMATH DE number 1980940 (Why is no real title available?)
• scientific article; zbMATH DE number 2081101 (Why is no real title available?)
• scientific article; zbMATH DE number 1927414 (Why is no real title available?)
• scientific article; zbMATH DE number 1798185 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• scientific article; zbMATH DE number 2086505 (Why is no real title available?)
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• scientific article; zbMATH DE number 2102730 (Why is no real title available?)
• scientific article; zbMATH DE number 3291623 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Java bytecode verification: Algorithms and formalizations
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Verified bytecode verifiers.
• Verified lightweight bytecode verification

Cited in

(24)

• A type system for the Java bytecode language and verifier
• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• Bytecode verification by model checking
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Verified bytecode verifiers.
• Certifying compilation and run-time code generation
• scientific article; zbMATH DE number 1701360 (Why is no real title available?)
• scientific article; zbMATH DE number 2089402 (Why is no real title available?)
• scientific article; zbMATH DE number 1231622 (Why is no real title available?)
• scientific article; zbMATH DE number 1956459 (Why is no real title available?)
• scientific article; zbMATH DE number 1746459 (Why is no real title available?)
• scientific article; zbMATH DE number 2165694 (Why is no real title available?)
• scientific article; zbMATH DE number 2090288 (Why is no real title available?)
• Algebraic compilation of safety-critical Java bytecode
• A type system for certified binaries
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• Verified just-in-time compiler on x86
• Programming Languages and Systems
• Formalisation and implementation of an algorithm for bytecode verification of \@NonNull types
• A Bytecode Logic for JML and Types
• Fundamental Approaches to Software Engineering
• A Completely Verified Realistic Bootstrap Compiler
• A Certified Lightweight Non-interference Java Bytecode Verifier
• \textsc{Mnemonics}: type-safe bytecode generation at run time

Describes a project that uses

Uses Software

• Isabelle/HOL
• TALx86

This page was built for publication: Verified bytecode verification and type-certifying compilation

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