Research

Programming Language Research Group (PLRG) aims to help developers design and implement high-quality software using diverse programming language technologies, including:

  • program analysis for automatically understanding program behaviors and detecting bugs and vulnerabilities.
  • mechanized specification to fill the gap between human-readable specifications and machine-friendly software.
  • program synthesis to lessen the burden of software development by automatically generating programs.
  • automated testing to generate test cases for software automatically on behalf of humans.

Recent Research Topics

JavaScript Mechanized Specifications

JavaScript is the most active programming language in GitHub. Every web browser contains a JavaScript engine. Its annually released specification, ECMA-262, defines the language syntax and semantics rigorously. It is also equipped with Test262, the implementation conformance test suite. However, manually maintaining the correctness of the fast-evolving language specification is challenging, even with the huge test suite. To reduce the gaps between the latest ECMA-262 and its implementations, we introduced a tool named ESMeta. It automatically extracts a JavaScript mechanized specification from ECMA-262 and generates various language-based tools by leveraging it, such as interpreters, conformance test synthesizers, specification type checkers, and program static analyzers.

ESMeta

Parametric Static Analysis

Static analysis is based on abstract interpretation and approximately estimates program behaviors using abstract semantics. While dynamic analysis collects runtime behaviors of instrumented code, static analysis over-approximates all program behaviors without actually executing programs. The static analysis quality is often evaluated by three criteria:

  • Performance denotes how fast static analysis analyzes programs.
  • Precision stands for the accuracy of analysis results.
  • Soundness represents whether analysis results cover all possible program behaviors at runtime.

Diverse analysis techniques have been proposed to enhance the performance and precision of static analysis while preserving soundness. Researchers have proposed parametric static analysis to mechanically select analysis parameters depending on given programs and analysis purposes. We surveyed analysis parameters and their parameter selection in the literature. In addition, we presented new analysis parameters and new parameter selection approaches.

Static Analysis

Search