Java bytecode verification: Algorithms and formalizations

DOI10.1023/A:1025055424017MaRDI QIDQ1405988zbMATH OpenOpenAlexFDO

Authors Xavier Leroy

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:1025055424017

zbMATH Keywords

abstract interpretationbytecode verificationsubroutinesdataflow analysisJava Virtual Machine

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1798185
• Fundamental Approaches to Software Engineering
• Bytecode verification on Java smart cards
• scientific article; zbMATH DE number 1857507
• Lightweight bytecode verification

Cited in

(38)

• Algebraic compilation of safety-critical Java bytecode
• Theorem Proving in Higher Order Logics
• Bytecode verification on Java smart cards
• Instruction-level security analysis for information flow in stack-based assembly languages
• scientific article; zbMATH DE number 2087852 (Why is no real title available?)
• scientific article; zbMATH DE number 1798185 (Why is no real title available?)
• Formal specification and verification of JDK's identity hash map implementation
• scientific article; zbMATH DE number 2087509 (Why is no real title available?)
• A formally verified compiler back-end
• scientific article; zbMATH DE number 2087564 (Why is no real title available?)
• scientific article; zbMATH DE number 2030038 (Why is no real title available?)
• Certificate size reduction in abstraction-carrying code
• Abstraction-carrying code: a model for mobile code safety
• Using abstract interpretation to add type checking for interfaces in Java bytecode verification
• Formalization and analysis of class loading in Java
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• scientific article; zbMATH DE number 2087621 (Why is no real title available?)
• scientific article; zbMATH DE number 2102730 (Why is no real title available?)
• A certified lightweight non-interference Java bytecode verifier
• Tool-assisted specification and verification of typed low-level languages
• Byte code level cross-compilation for developing web applications
• Security types preserving compilation
• Formalizing non-interference for a simple bytecode language in Coq
• Lightweight bytecode verification
• Improving the official specification of Java bytecode verification
• Verified bytecode verification and type-certifying compilation
• Rule-based programming in Java for protocol verification
• scientific article; zbMATH DE number 1857507 (Why is no real title available?)
• Security monitor inlining and certification for multithreaded Java
• scientific article; zbMATH DE number 5499373 (Why is no real title available?)
• Verified bytecode subroutines
• scientific article; zbMATH DE number 1980953 (Why is no real title available?)
• Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types
• Bytecode verification by model checking
• Provably correct runtime monitoring
• scientific article; zbMATH DE number 1796120 (Why is no real title available?)
• Verification of Java Programs with Generics
• Formal specification and verification of JDK's identity hash map implementation

This page was built for publication: Java bytecode verification: Algorithms and formalizations

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