Memory model sensitive bytecode verification

DOI10.1007/S10703-007-0041-6MaRDI QIDQ2461564zbMATH OpenOpenAlexFDO

Authors Thuan Quang Huynh, Abhik Roychoudhury

Publication date 28 November 2007

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-007-0041-6

zbMATH Keywords

Bytecode verificationProgramming language memory modelsSoftware model checking

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Java Memory Model-Aware Model Checking
• The Java memory model
• Verification of Concurrent Programs on Weak Memory Models
• Plan B, a buffered memory model for Java
• Bytecode verification by model checking

Cites work

• Computer Aided Verification
• Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• scientific article; zbMATH DE number 4082934 (Why is no real title available?)
• scientific article; zbMATH DE number 107700 (Why is no real title available?)
• Maximal Flow Through a Network
• The Java memory model

Cited in

(4)

• Bytecode verification by model checking
• Formal specification and verification of the C\(\#\) thread model
• Plan B, a buffered memory model for Java
• Sound and complete monitoring of sequential consistency for relaxed memory models

Describes a project that uses

Uses Software

• Checkfence

This page was built for publication: Memory model sensitive bytecode verification

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