The LET Project: program analysis for smalL/safE/smarT code


ROPAS: Research On Program Analysis System
National Creative Research Initiatives Center
Seoul National University
[Korean]

Principal investigator: Kwangkeun Yi

Goal

A completely new computing environment emerges when all the computers around the globe are connected via a light-speed network. All of the code for a particular program will not necessarily be ready beforehand in a host computer. Code fragments are dispersed across the globe and will be brought to a host via the light-speed network just when they are needed for the host program's continuation. In the global computing environment an extremely large number of such code fragments will compete for providing the optimal functionality to the hosts in need.

Our goal is to achieve compiler technologies for this global computing environment of the future. In particular, we will focus on the following three compilation problems for higher-order & typed programming languages like ML:

Approach

Our research hypothesis is that semantic-based static analysis will play the key role in solving the above three compilation problems. Static analysis is the technique of estimating the input program's run-time properties before execution. By ``semantic-based,'' we mean that the analysis has to be based on programming language's semantic foundations (e.g. various formalisms of semantics specifications, type theories, computational logics and models, and etc.). Firm foot on formal foundations of the source programming languages will enable us to clearly understand the fundamental structures of the static analysis problems and hence help us to avoid unsound and ad-hoc solutions.

The semantic-based static analysis will be essential in solving the three problems as follows:

Our research position is to aggressively adopt recent progress in programming language theories into a set of practical compilation techniques. The major thrust for promoting the potential synergy between the language theories and compilation practices comes from our focus on semantic-based static analysis.

Members/Publications/Softwares