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

JavaTheorem provingJVMCompilerBytecode verification

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

• 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?)
• Hoare logic for Java in Isabelle/HOL
• 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
• \(\mu\)Java: Embedding a programming language in a theorem prover

Cited in

(22)

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

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)