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