BicolanoMT: a formalization of multi-threaded Java at bytecode level. This paper describes a formalization of multi-threaded Java bytecode in Coq. The formalization builds on the existing Bicolano formalization for sequential Java byte- code – which captures basically all aspects of sequential bytecode supported by the CLDC (Java for mobile phones) platform. We use a special extension framework to extend the existing formalization in a systematic way. The formalization is com- plete: it models all aspects related to concurrency: monitors, thread start and completion, the wait-notify mechanism and the interrupt mechanism, and it does not require any transformation of the bytecode. The formalization is developed to be suited for program verification and static analysis.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element