Java bytecode verification: Algorithms and formalizations
From MaRDI portal
Publication:1405988
DOI10.1023/A:1025055424017zbMath1031.68041OpenAlexW1501401133MaRDI QIDQ1405988
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
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Verified bytecode verification and type-certifying compilation ⋮ Certificate size reduction in abstraction-carrying code ⋮ Instruction-level security analysis for information flow in stack-based assembly languages ⋮ Provably correct runtime monitoring ⋮ Tool-assisted specification and verification of typed low-level languages ⋮ Security types preserving compilation ⋮ A formally verified compiler back-end ⋮ Formalizing non-interference for a simple bytecode language in Coq ⋮ Abstraction-carrying code: a model for mobile code safety ⋮ Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types ⋮ Security monitor inlining and certification for multithreaded Java ⋮ Using abstract interpretation to add type checking for interfaces in Java bytecode verification ⋮ Byte code level cross-compilation for developing web applications
