BicolanoMT: a Formalization of Multi-Threaded Java at Bytecode Level 1
Gustavo Petri, Marieke Huisman · 2008
This paper describes a formalization of multi-threaded Java bytecode in Coq. The formalization builds on the existing Bicolano formalization for sequential Java bytecode ‐ 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 complete: 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.