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.

Economic Development of Urban Areas

In this dissertation I study the development of urban areas. At the aggregate level I investigate how they may be affected by climate change policies and by being designated the seat of governmental power. At the household level I study with coauthors how microfinance could improve the health of urban residents. In Chapter 1, I investigate how local employment may be affected by electricity price increases, which is a likely consequence of climate change policies. I outline how previous studies that find large, negative effects may be biased. To overcome these biases I develop a novel estimation strategy that blends border-pair regressions with the synthetic control methodology. I show the conditions for consistent estimation. Using this estimator, I find no effect of contemporaneous price changes on employment. Consistent with the longer time-frame for manufacturing decisions, I do find evidence for negative effects from perceived permanent price shocks. These estimates are much smaller than previous research has found. National capital cities are often substantially larger than other cities in their countries. In Chapter 2, I investigate whether there is a causal effect from being a capital by studying the 1960 relocation of the Brazilian capital from Rio de Janeiro to Brasília. Using a synthetic controls strategy I find that losing the capital had no significant effects on Rio de Janeiro in terms of population, employment, or gross domestic product (GDP). I find that Brasília experienced large and significant increases in population, employment, and GDP. I find evidence of large spillovers from the public to the private sector. Chapter 3 investigates how microfinance could increase the uptake of costly health goods. We study the effect of time payments (micro-loans or micro-savings) on willingness-to-pay (WTP) for a water filter among households in the slums of Dhaka, Bangladesh. We find that time payments significantly increase WTP: compared to a lump-sum up-front purchase, median WTP increases 83% with a six-month loan and 115% with a 12-month loan. We find that households are quite patient with respect to consumption of health inputs. We find evidence for the presence of credit and savings constraints.