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
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
- Lochbihler, Andreas: Verifying a compiler for Java threads (2010)
- Dabrowski, Frédéric; Pichardie, David: A certified data race analysis for a Java-like language (2009)