The current definition of the Java Bytecode Verifier, as well as the
proposals to formalize it, do not include any check about consistency of critical sections (those between
monitorenter and monitorexit instructions).
So code is run, even if the nesting of critical sections is corrupted.
In this paper we isolate a sublanguage of the Java Virtual Machine
with thread creation and mutual exclusion. For this subset we
define a semantics and a formal verifier that enforces basic
properties of threads and critical sections.
Our verifier integrates well with previous formalizations of the Java
Bytecode Verifier.
