A dozen instructions make Java bytecode

Prelegent(ci)

Patryk Czarnik

Afiliacja

Uniwersytet Warszawski

Termin

15 marca 2010 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Prerun przed Bytecode 2010.

Abstrakt pracy:

  One of the biggest obstacles in the formalisation of the Java
  bytecode is that the language consists of 200 instructions.
  However, a rigorous handling of a programming language in the
  context of program verification and error detection requires a
  formalism which is compact in size.  Therefore, the actual Java
  bytecode instruction set is never used in the context.  Instead, the
  existing formalisations usually cover a `representative' set of
  instructions.  This paper describes how to reduce the number of
  instructions in a systematic and rigorous way into a manageable set
  of more general operations that cover the full functionality of the
  Java bytecode. The factorisation of the instruction set is based on
  the use of the runtime structures such as operand stack, heap etc.
  This is achieved by presentation of a formal semantics for the Java
  Virtual Machine.

---