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 talk 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.

Authors: Gaetano Bigliardi, Cosimo Laneve

ASTEC seminar
June 20, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 13.15 - 14.00 (+ coffee and discussion)

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.