Verified lightweight bytecode verification

DOI10.1002/CPE.597MaRDI QIDQ4329632zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

Java virtual machine

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

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

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

Describes a project that uses

Uses Software

• Isar
• Isabelle/HOL
• Isabelle

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)