Bytecode verification by model checking

DOI10.1023/A:1025059508087MaRDI QIDQ1405996zbMATH OpenFDO

Authors Stefan Friedrich, Marek Gawkowski, David Basin

Publication date 9 September 2003

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

zbMATH Keywords

model checkingstatic analysisbytecode verificationtype safety

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 1927414
• scientific article; zbMATH DE number 2087621
• Memory model sensitive bytecode verification
• scientific article; zbMATH DE number 1701360
• scientific article; zbMATH DE number 2102730
• Verified bytecode verification and type-certifying compilation
• Fundamental Approaches to Software Engineering
• Java bytecode verification: Algorithms and formalizations
• Lightweight bytecode verification

Cited in

(15)

• Verified lightweight bytecode verification
• A local approach for temporal model checking of Java bytecode
• Computer Science Logic
• Computer Aided Verification
• Computer Aided Verification
• Faster and more complete extended static checking for the Java modeling language
• Fundamental Approaches to Software Engineering
• Verified bytecode verifiers.
• Using abstract interpretation to add type checking for interfaces in Java bytecode verification
• scientific article; zbMATH DE number 1927414 (Why is no real title available?)
• scientific article; zbMATH DE number 2087621 (Why is no real title available?)
• scientific article; zbMATH DE number 2102730 (Why is no real title available?)
• Memory model sensitive bytecode verification
• scientific article; zbMATH DE number 1701360 (Why is no real title available?)
• Verified bytecode subroutines

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL

This page was built for publication: Bytecode verification by model checking

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