Plant Migrations Impact on Potential Vegetation and Carbon Redistribution in Northern North America from Climate Change

Forests have a prominent role in carbon storage and sequestration. Anthropogenic forcing has the potential to accelerate climate change and alter the distribution of forests. How forests redistribute spatially and temporally in response to climate change can alter their carbon sequestration potential. The driving question for this research was: How does plant migration from climate change impact vegetation distribution and carbon sequestration potential over continental scales? Large-scale simulation of the equilibrium response of vegetation and carbon from future climate change has shown relatively modest net gains in sequestration potential, but studies of the transient response has been limited to the sub-continent or landscape scale. The transient response depends on fine scale processes such as competition, disturbance, landscape characteristics, dispersal, and other factors, which makes it computational prohibitive at large domain sizes. To address this, this research used an advanced mechanistic model (Ecosystem Demography Model, ED) that is individually based, but pseudo-spatial, that reduces computational intensity while maintaining the fine scale processes that drive the transient response. First, the model was validated against remote sensing data for current plant functional type distribution in northern North America with a current climatology, and then a future climatology was used to predict the potential equilibrium redistribution of vegetation and carbon from future climate change. Next, to enable transient calculations, a method was developed to simulate the spatially explicit process of dispersal in pseudo-spatial modeling frameworks. Finally, the new dispersal sub-model was implemented in the mechanistic ecosystem model, and a model experimental design was designed and completed to estimate the transient response of vegetation and carbon to climate change. The potential equilibrium forest response to future climate change was found to be large, with large gross changes in distribution of plant functional types and comparatively smaller changes in net carbon sequestration potential for the region. However, the transient response was found to be on the order of centuries, and to depend strongly on disturbance rates and dispersal distances. Future work should explore the impact of species-specific disturbance and dispersal rates, landscape fragmentation, and other processes that influence migration rates and have been simulated at the sub-continent scale, but now at continental scales, and explore a range of alternative future climate scenarios as they continue to be developed.

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.