Verified lightweight bytecode verification

DOI10.1002/cpe.597zbMath0997.68018OpenAlexW2096228713MaRDI QIDQ4329632

Tobias Nipkow, Gerwin Klein

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)

Related Items (5)

Verified bytecode verification and type-certifying compilation ⋮ Type systems equivalent to data-flow analyses for imperative languages ⋮ 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,

Uses Software

• Isabelle
• Isabelle/HOL
• Isar

Cites Work

• Unnamed Item
• Isabelle. A generic theorem prover

This page was built for publication: Verified lightweight bytecode verification