FRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKS

Symbolic execution is a powerful program analysis technique, but it is very challenging to apply to programs built using event-driven frameworks, such as Android. The main reason is that the framework code itself is too complex to symbolically execute. The standard solution is to manually create a framework model that is simpler and more amenable to symbolic execution. However, developing and maintaining such a model by hand is difficult and error-prone. We claim that we can leverage program synthesis to introduce a high-degree of automation to the process of framework modeling. To support this thesis, we present three pieces of work. First, we introduced SymDroid, a symbolic executor for Android. While Android apps are written in Java, they are compiled to Dalvik bytecode format. Instead of analyzing an app’s Java source, which may not be available, or decompiling from Dalvik back to Java, which requires significant engineering effort and introduces yet another source of potential bugs in an analysis, SymDroid works directly on Dalvik bytecode. Second, we introduced Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket takes as input the framework API and tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes an executable framework model by instantiating design patterns, such that the behavior of a synthesized model on the tutorial programs matches that of the original framework. Lastly, in order to scale program synthesis to framework models, we devised adaptive concretization, a novel program synthesis algorithm that combines the best of the two major synthesis strategies: symbolic search, i.e., using SAT or SMT solvers, and explicit search, e.g., stochastic enumeration of possible solutions. Adaptive concretization parallelizes multiple sub-synthesis problems by partially concretizing highly influential unknowns in the original synthesis problem. Thanks to adaptive concretization, Pasket can generate a large-scale model, e.g., thousands lines of code. In addition, we have used an Android model synthesized by Pasket and found that the model is sufficient to allow SymDroid to execute a range of apps.

Scenic Design of James and the Giant Peach

The purpose of this thesis is to provide research, supporting paperwork, production photographs and other materials that document the scenic design process for James and the Giant Peach at Adventure Theatre MTC. This thesis contains the following: concept statement, scenic research images collected to express location, and the emotional/ intellectual/ psychological landscapes for the production, preliminary sketches, photographs of the ¼” scale model, drafting plates and supporting paint elevations to communicate the design, prop list and accompanying research, archival production photographs to document the completed design, and finally periodical reviews of the show.

Troilus and Cressida - A Scenic Design

The purpose of this thesis is to provide research, supporting paperwork, production photographs, and other materials that document the scenic design process for the production of William Shakespeare’s Troilus & Cressida by the University of Maryland – College Park, School of Theater, Dance, and Performance Studies. This thesis contains the following: scenic research images collected to express period, location, and emotional/intellectual landscapes to the production team; preliminary sketches; photographs of the ¼” scale model; a full set of drafting plates and paint elevations used to communicate the design to the technical director and paint charge; a unit list naming each scenic element; a props list and research book to detail each hand prop, furniture piece and consumable to the prop master; and, lastly, archival production photographs to document the completed design.