Date of Award

Spring 1-1-2014

Document Type


Degree Name

Doctor of Philosophy (PhD)


Electrical, Computer & Energy Engineering

First Advisor

Bor-Yuh E. Chang

Second Advisor

Sriram Sankaranarayanan

Third Advisor

Xavier Rival

Fourth Advisor

Anders Møller

Fifth Advisor

Jeremy Siek


For commercial development, dynamic languages are growing in popularity. Consequently, dynamic language developers must consider the correctness of their code. Deployment of correct or sufficiently correct code is critical to the success and adoption of that code. However, it is challenging to ensure the correctness of dynamic language code when it is a library. Inputs to dynamic language libraries are often not simple values. They can also be open objects, which permit adding, removing, and iterating over attribute names, and they can be functions that may be called. Furthermore, the result of running library functions on objects is often new objects derived from the input objects.

To ensure the correctness of dynamic language libraries, this dissertation uses static analysis. Static analysis is typically used to infer facts about programs' values, but in these dynamic language libraries, values can be objects and functions. These objects may be unknown and thus have an unknown set of attribute names because they are inputs or these objects may be iteratively derived from other objects. Functions may be stored, called, or wrapped in other functions, regardless of if they are known or not. A static analysis for dynamic language libraries must handle these cases.

To support static analysis of libraries, this dissertation introduces local heap abstractions suitable for representing parts of memory that library code may affect. These abstractions build upon abstractions for sets that enable representing relations between attribute names of otherwise unknown objects. Furthermore, the local reasoning is utilized to abstract the effect of calling unknown functions.

The precision of these abstractions are demonstrated on a range of small, but complex JavaScript-inspired examples. The examples are extracted from libraries such as Traits.js and Google Closure.