Verified lightweight bytecode verification

DOI10.1002/CPE.597zbMATH Open0997.68018OpenAlexW2096228713MaRDI QIDQ4329632FDOQ4329632

Authors: Gerwin Klein, Tobias Nipkow 

Publication date: 1 May 2002

Published in: Concurrency and Computation: Practice and Experience (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/cpe.597

Recommendations

• scientific article; zbMATH DE number 1701360
• Verified bytecode verifiers.
• Lightweight bytecode verification
• scientific article; zbMATH DE number 1927414
• Bytecode verification by model checking

zbMATH Keywords

Java virtual machine

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Cites Work

• Isabelle. A generic theorem prover
• \(\mu\)Java: Embedding a programming language in a theorem prover

Cited In (7)

• Lightweight bytecode verification
• Type systems equivalent to data-flow analyses for imperative languages
• Verified bytecode verification and type-certifying compilation
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Java access protection through typing
• Modular development of certified program verifiers with a proof assistant,
• \textsc{Mnemonics}: type-safe bytecode generation at run time

Uses Software

• Isabelle
• Isabelle/HOL
• Isar

This page was built for publication: Verified lightweight bytecode verification

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