SAFE 2.0

Scalable Analysis Framework for ECMAScript

SAFE 2.0 is a scalable and pluggable analysis framework for JavaScript web applications.


JavaScript IR-based Semantics Extraction Toolchain

JISET is JavaScript IR-based Semantics Extraction Toolchain. It synthesizes a JavaScript parser for a given grammar written in BNF_ES, an extended BNF used in ECMAScript. It also automatically extracts semantics using rule-based compilation.


Static Analysis Framework for Android Hybrid Applications

HybriDroid is a static analysis framework for Android hybrid applications. We investigated the semantics of Android hybrid applications especially for the interoperation mechanism of Android Java and JavaScript. Then, we designed and implemented a static analysis framework that analyzes inter-communication between Android Java and JavaScript.

Multilingual Static Analysis

Semantic Summary Extraction from C Code for JNI Program Analysis

We proposed a novel approach to analyze multilingual programs statically. Unlike existing approaches that extend a static analyzer for a host language to support analysis of foreign function calls, our approach extracts semantic summaries from programs written in guest languages using a modular analysis tech- nique, and performs a whole-program analysis with the extracted semantic summaries.

Multiple Dispatch

Symmetric Multiple Dispatch Semantics for Languages with Parametric Polymorphism and Variance

We presented the first formal specification of a strongly typed object-oriented language with symmetric multiple dispatch, multiple inheritance, and parametric polymorphism with variance. We defined both a static (type-checking) semantics and a dynamic (dispatching) semantics and prove the type soundness of the language, thus demonstrating that our novel dynamic dispatch algorithm is consistent with the static semantics.