Verified bytecode subroutines

DOI10.1023/A:1025095122199MaRDI QIDQ1405993zbMATH OpenOpenAlexFDO

Authors M. Wildmoser, Gerwin Klein

Publication date 9 September 2003

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1025095122199

zbMATH Keywords

theorem provingJavaIsabellebytecode verificationsubroutinesdataflow analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1701360
• Verified bytecode verifiers.
• Bytecode verification by model checking
• scientific article; zbMATH DE number 1927414
• Java bytecode verification: Algorithms and formalizations

Cited in

(6)

• scientific article; zbMATH DE number 1701360 (Why is no real title available?)
• Formal verification of C systems code. Structured types, separation logic and theorem proving
• Tool-assisted specification and verification of typed low-level languages
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• scientific article; zbMATH DE number 2087564 (Why is no real title available?)
• Verified bytecode verifiers.

Describes a project that uses

Uses Software

• Isabelle/HOL
• Isabelle

This page was built for publication: Verified bytecode subroutines

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