ESSAYS IN ENERGY, ENVIRONMENT AND TECHNOLOGICAL CHANGE

This dissertation studies technological change in the context of energy and environmental economics. Technology plays a key role in reducing greenhouse gas emissions from the transportation sector. Chapter 1 estimates a structural model of the car industry that allows for endogenous product characteristics to investigate how gasoline taxes, R&D subsidies and competition affect fuel efficiency and vehicle prices in the medium-run, both through car-makers' decisions to adopt technologies and through their investments in knowledge capital. I use technology adoption and automotive patents data for 1986-2006 to estimate this model. I show that 92% of fuel efficiency improvements between 1986 and 2006 were driven by technology adoption, while the role of knowledge capital is largely to reduce the marginal production costs of fuel-efficient cars. A counterfactual predicts that an additional $1/gallon gasoline tax in 2006 would have increased the technology adoption rate, and raised average fuel efficiency by 0.47 miles/gallon, twice the annual fuel efficiency improvement in 2003-2006. An R&D subsidy that would reduce the marginal cost of knowledge capital by 25% in 2006 would have raised investment in knowledge capital. This subsidy would have raised fuel efficiency only by 0.06 miles/gallon in 2006, but would have increased variable profits by $2.3 billion over all firms that year. Passenger vehicle fuel economy standards in the United States will require substantial improvements in new vehicle fuel economy over the next decade. Economic theory suggests that vehicle manufacturers adopt greater fuel-saving technologies for vehicles with larger market size. Chapter 2 documents a strong connection between market size, measured by sales, and technology adoption. Using variation consumer demographics and purchasing pattern to account for the endogeneity of market size, we find that a 10 percent increase in market size raises vehicle fuel efficiency by 0.3 percent, as compared to a mean improvement of 1.4 percent per year over 1997-2013. Historically, fuel price and demographic-driven market size changes have had large effects on technology adoption. Furthermore, fuel taxes would induce firms to adopt fuel-saving technologies on their most efficient cars, thereby polarizing the fuel efficiency distribution of the new vehicle fleet.

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.