Table of Contents
Three Invited Talks
When? Friday November 9th 2012 at 14:00 to 16:00
Where? room 0.2.13 at Selma Lagerlöfs Vej 300, 9220 Aalborg Ø.
Talk 1:
Speaker: Professor Peter H. Schmitt, Karlsruhe Institute of Technology, Germany.
Title: Deductive Verification of Information Flow Properties in Java
Abstract:
The presentation starts with a short introduction into deductive program verification. This verification needs as input Java source code annotated with JML (Java Modelling Language) specifications. From these proof obligations in a program logic will automatically be generated, in our case proof obligations in an instance of Dynamic Logic. The KeY verification systems serve as a guiding example. In the main part of the talk we will consider information leakage as one of the most frequent information flow properties and discuss its formalization in Dynamic Logic. The solution finally adopted is usually referred to as “self‐composition”. It is shown how “self‐composition” can be realized in the KeY system. A small example concludes the presentation.
Talk 2:
Speaker: Dr. Isabel Tonin, Compiler Expert, Aicas GmbH, Karlsruhe, Germany
Title: Towards Rule Driven Compilation: an Overview of JamaicaVM's New Bytecode Compiler
Abstract:
In the scope of Charter*, an ARTEMIS Embedded Computing Systems Initiative project, a Java specific rule driven graph transformation tool called RDT was developed by the University of Twente (Netherlands). Also within the project this tool was used for implementing the new JamaicaVM* rule based compiler. Compilation in Jamaica is done in three phases as follows. First a Java bytecode method is translated into an intermediate representation, in a form of a Control Flow Graph (CFG). Then the optimizations, including the ones expressed as RDT rules, are applied. Finally, from this optimized graph code is generated. In this talk, an overview of this compiler shall be presented with emphasis on the rule driven optimizations. The talk includes the underlying concepts used for implementing the compiler, such as static single assignment (SSA) and dominance relation, as well as optimizations, such as data flow analysis (DFA) and tail recursion * CHARTER ‐ Critical and High Assurance Requirements Transformed through Engineering Rigour (see http://charter‐project.net/) a paper describing the tool can be found at wwwhome.ewi.utwente.nl/~rensink/papers/fase2012.pdf * the Aicas GmbH (Germany) realtime Java Virtual Machine (see http://www.aicas.com/)
See the full programme on http://infinit.dk/dk/nyheder_og_arrangementer/arrangementer/java_two_phd_defences_and_talks_given_by_committee_members.htm
Talk3:
Speaker: Dr. James Hunt, CEO, Aicas GmbH, Karlsruhe, Germany
Title: Safety-Critical Applications in Java
Abstract:
New standards for the certification of avionics software now facilitate the use of object-oriented technology and provide guidance for dynamic memory management. This provides the basis for using Realtime Java with deterministic garbage collection in these systems. This talk will describe these changes and discuss what is necessary to qualify a Realtime Java implementation for avionics systems. This will include a detailed discussion of object-oriented features and garbage collection with respect to certification.