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.

A Binary Classifier for Test Case Feasibility Applied to Automatically Generated Tests of Event-Driven Software

Modern software application testing, such as the testing of software driven by graphical user interfaces (GUIs) or leveraging event-driven architectures in general, requires paying careful attention to context. Model-based testing (MBT) approaches first acquire a model of an application, then use the model to construct test cases covering relevant contexts. A major shortcoming of state-of-the-art automated model-based testing is that many test cases proposed by the model are not actually executable. These \textit{infeasible} test cases threaten the integrity of the entire model-based suite, and any coverage of contexts the suite aims to provide. In this research, I develop and evaluate a novel approach for classifying the feasibility of test cases. I identify a set of pertinent features for the classifier, and develop novel methods for extracting these features from the outputs of MBT tools. I use a supervised logistic regression approach to obtain a model of test case feasibility from a randomly selected training suite of test cases. I evaluate this approach with a set of experiments. The outcomes of this investigation are as follows: I confirm that infeasibility is prevalent in MBT, even for test suites designed to cover a relatively small number of unique contexts. I confirm that the frequency of infeasibility varies widely across applications. I develop and train a binary classifier for feasibility with average overall error, false positive, and false negative rates under 5\%. I find that unique event IDs are key features of the feasibility classifier, while model-specific event types are not. I construct three types of features from the event IDs associated with test cases, and evaluate the relative effectiveness of each within the classifier. To support this study, I also develop a number of tools and infrastructure components for scalable execution of automated jobs, which use state-of-the-art container and continuous integration technologies to enable parallel test execution and the persistence of all experimental artifacts.

INTIMATE APPAREL: AN EXPLORATION OF COSTUME DESIGN IDEAS AND PROCESS FOR THE UNIVERSITY OF MARYLAND’S DEPARTMENT OF THEATRE, DANCE AND PERFORMING 2015 PRODUCTION

The following thesis navigates the primary artistic concept, design process and execution of Marchlena Rodgers’ costume design for the University of Maryland’s production of Intimate Apparel. Intimate Apparel opened October 9, 2015 in the University of Maryland’s Kay Theatre. The piece was written by Lynn Nottage directed by Jennifer Nelson. The set was designed by Lydia Francis, Lighting was designed by Max Doolittle.

Action and perception: Neural indices of learning in infants

Early human development offers a unique perspective in investigating the potential cognitive and social implications of action and perception. Specifically, during infancy, action production and action perception undergo foundational developments. One essential component to examine developments in action processing is the analysis of others’ actions as meaningful and goal-directed. Little research, however, has examined the underlying neural systems that may be associated with emerging action and perception abilities, and infants’ learning of goal-directed actions. The current study examines the mu rhythm—a brain oscillation found in the electroencephalogram (EEG)—that has been associated with action and perception. Specifically, the present work investigates whether the mu signal is related to 9-month-olds’ learning of a novel goal-directed means-end task. The findings of this study demonstrate a relation between variations in mu rhythm activity and infants’ ability to learn a novel goal-directed means-end action task (compared to a visual pattern learning task used as a comparison task). Additionally, we examined the relations between standardized assessments of early motor competence, infants’ ability to learn a novel goal-directed task, and mu rhythm activity. We found that: 1a) mu rhythm activity during observation of a grasp uniquely predicted infants’ learning on the cane training task, 1b) mu rhythm activity during observation and execution of a grasp did not uniquely predict infants’ learning on the visual pattern learning task (comparison learning task), 2) infants’ motor competence did not predict infants’ learning on the cane training task, 3) mu rhythm activity during observation and execution was not related to infants’ measure of motor competence, and 4) mu rhythm activity did not predict infants’ learning on the cane task above and beyond infants’ motor competence. The results from this study demonstrate that mu rhythm activity is a sensitive measure to detect individual differences in infants’ action and perception abilities, specifically their learning of a novel goal-directed action.

THE INFLUENCE OF MOTIVATION ON EMOTION REGULATION AND MOTOR PERFORMANCE: EXAMINATION OF A NEURO-AFFECTIVE MODEL

Mental stress is known to disrupt the execution of motor performance and can lead to decrements in the quality of performance, however, individuals have shown significant differences regarding how fast and well they can perform a skilled task according to how well they can manage stress and emotion. The purpose of this study was to advance our understanding of how the brain modulates emotional reactivity under different motivational states to achieve differential performance in a target shooting task that requires precision visuomotor coordination. In order to study the interactions in emotion regulatory brain areas (i.e. the ventral striatum, amygdala, prefrontal cortex) and the autonomic nervous system, reward and punishment interventions were employed and the resulting behavioral and physiological responses contrasted to observe the changes in shooting performance (i.e. shooting accuracy and stability of aim) and neuro-cognitive processes (i.e. cognitive load and reserve) during the shooting task. Thirty-five participants, aged 18 to 38 years, from the Reserve Officers’ Training Corp (ROTC) at the University of Maryland were recruited to take 30 shots at a bullseye target in three different experimental conditions. In the reward condition, $1 was added to their total balance for every 10-point shot. In the punishment condition, $1 was deducted from their total balance if they did not hit the 10-point area. In the neutral condition, no money was added or deducted from their total balance. When in the reward condition, which was reportedly most enjoyable and least stressful of the conditions, heart rate variability was found to be positively related to shooting scores, inversely related to variability in shooting performance and positively related to alpha power (i.e. less activation) in the left temporal region. In the punishment (and most stressful) condition, an increase in sympathetic response (i.e. increased LF/HF ratio) was positively related to jerking movements as well as variability of placement (on the target) in the shots taken. This, coupled with error monitoring activity in the anterior cingulate cortex, suggests evaluation of self-efficacy might be driving arousal regulation, thus affecting shooting performance. Better performers showed variable, increasing high-alpha power in the temporal region during the aiming period towards taking the shot which could indicate an adaptive strategy of engagement. They also showed lower coherence during hit shots than missed shots which was coupled with reduced jerking movements and better precision and accuracy. Frontal asymmetry measures revealed possible influence of the prefrontal lobe in driving this effect in reward and neutral conditions. The possible interactions, reasons behind these findings and implications are discussed.