Institute of Computer Languages
Compilers and Languages Group
|Date:||Wednesday, June 16, 2004|
|Location:||TU Wien, building at the Freihaus, FH HS 4, Wiedner Hauptstraße 8, Turm B, yellow area, 2nd upper floor|
We propose a novel verification algorithm based on Static Single Assignment form (SSA). For each value we match the type it is defined with against the type of each of the values uses. Interadjacent transitions of a value through stack and registers no longer have to be verified explicitly, as their correctness can be induced once the data flow from definition to all uses is known to be type-safe.
Our verification algorithm is more efficient than the traditional bytecode verifier, as it is also beneficial to later stages in the compilation pipeline. Whereas traditional JVMs treat the verifier as a black box and discard information gained during the DFA, our algorithm constructs an SSA-based representation of the program that can be re-used by optimizing just-in-time compilers often found in modern JVMs.
Dr. Probst earned his Ph.D. in Computer Science from the Universität des Saarlandes, Saarbrücken, Germany.