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