Static analysis of programs is a proven technology in the implementation of compilers and interpreters. Recent years have begun to see application of static analysis techniques in novel areas such as software validation and software re-engineering. This project will demonstrate that static analysis technology facilitates the validation of systems based on the internet and on smart cards.

A brief presentation of the project given to the Information Society Technology, and a two page description of the project.

Objectives

The objective of the project is to assess the scalability of static analysis technology to the validation of security and safety aspects of realistic languages and applications. We have identified two domains where security is all-important: smart cards and internet programming. We intend to develop methods that apply to both domains by focusing a substantial part of our efforts on the Java programming language and its dialect Java Card , treating source-level as well as bytecode-level applications.

The project has 4 main tasks: