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.

The Real-Quaternionic Indicator of Irreducible Self-Conjugate Representations of Real Reductive Algebraic Groups and A Comment on the Local Langlands Correspondence of GL(2, F )

The real-quaternionic indicator, also called the $\delta$ indicator, indicates if a self-conjugate representation is of real or quaternionic type. It is closely related to the Frobenius-Schur indicator, which we call the $\varepsilon$ indicator. The Frobenius-Schur indicator $\varepsilon(\pi)$ is known to be given by a particular value of the central character. We would like a similar result for the $\delta$ indicator. When $G$ is compact, $\delta(\pi)$ and $\varepsilon(\pi)$ coincide. In general, they are not necessarily the same. In this thesis, we will give a relation between the two indicators when $G$ is a real reductive algebraic group. This relation also leads to a formula for $\delta(\pi)$ in terms of the central character. For the second part, we consider the construction of the local Langlands correspondence of $GL(2,F)$ when $F$ is a non-Archimedean local field with odd residual characteristics. By re-examining the construction, we provide new proofs to some important properties of the correspondence. Namely, the construction is independent of the choice of additive character in the theta correspondence.

Learning Binary Code Representations for Effective and Efficient Image Retrieval

The size of online image datasets is constantly increasing. Considering an image dataset with millions of images, image retrieval becomes a seemingly intractable problem for exhaustive similarity search algorithms. Hashing methods, which encodes high-dimensional descriptors into compact binary strings, have become very popular because of their high efficiency in search and storage capacity. In the first part, we propose a multimodal retrieval method based on latent feature models. The procedure consists of a nonparametric Bayesian framework for learning underlying semantically meaningful abstract features in a multimodal dataset, a probabilistic retrieval model that allows cross-modal queries and an extension model for relevance feedback. In the second part, we focus on supervised hashing with kernels. We describe a flexible hashing procedure that treats binary codes and pairwise semantic similarity as latent and observed variables, respectively, in a probabilistic model based on Gaussian processes for binary classification. We present a scalable inference algorithm with the sparse pseudo-input Gaussian process (SPGP) model and distributed computing. In the last part, we define an incremental hashing strategy for dynamic databases where new images are added to the databases frequently. The method is based on a two-stage classification framework using binary and multi-class SVMs. The proposed method also enforces balance in binary codes by an imbalance penalty to obtain higher quality binary codes. We learn hash functions by an efficient algorithm where the NP-hard problem of finding optimal binary codes is solved via cyclic coordinate descent and SVMs are trained in a parallelized incremental manner. For modifications like adding images from an unseen class, we propose an incremental procedure for effective and efficient updates to the previous hash functions. Experiments on three large-scale image datasets demonstrate that the incremental strategy is capable of efficiently updating hash functions to the same retrieval performance as hashing from scratch.

Efficient Image and Video Representations for Retrieval

Image (Video) retrieval is an interesting problem of retrieving images (videos) similar to the query. Images (Videos) are represented in an input (feature) space and similar images (videos) are obtained by finding nearest neighbors in the input representation space. Numerous input representations both in real valued and binary space have been proposed for conducting faster retrieval. In this thesis, we present techniques that obtain improved input representations for retrieval in both supervised and unsupervised settings for images and videos. Supervised retrieval is a well known problem of retrieving same class images of the query. We address the practical aspects of achieving faster retrieval with binary codes as input representations for the supervised setting in the first part, where binary codes are used as addresses into hash tables. In practice, using binary codes as addresses does not guarantee fast retrieval, as similar images are not mapped to the same binary code (address). We address this problem by presenting an efficient supervised hashing (binary encoding) method that aims to explicitly map all the images of the same class ideally to a unique binary code. We refer to the binary codes of the images as `Semantic Binary Codes' and the unique code for all same class images as `Class Binary Code'. We also propose a new class­ based Hamming metric that dramatically reduces the retrieval times for larger databases, where only hamming distance is computed to the class binary codes. We also propose a Deep semantic binary code model, by replacing the output layer of a popular convolutional Neural Network (AlexNet) with the class binary codes and show that the hashing functions learned in this way outperforms the state­ of ­the art, and at the same time provide fast retrieval times. In the second part, we also address the problem of supervised retrieval by taking into account the relationship between classes. For a given query image, we want to retrieve images that preserve the relative order i.e. we want to retrieve all same class images first and then, the related classes images before different class images. We learn such relationship aware binary codes by minimizing the similarity between inner product of the binary codes and the similarity between the classes. We calculate the similarity between classes using output embedding vectors, which are vector representations of classes. Our method deviates from the other supervised binary encoding schemes as it is the first to use output embeddings for learning hashing functions. We also introduce new performance metrics that take into account the related class retrieval results and show significant gains over the state­ of­ the art. High Dimensional descriptors like Fisher Vectors or Vector of Locally Aggregated Descriptors have shown to improve the performance of many computer vision applications including retrieval. In the third part, we will discuss an unsupervised technique for compressing high dimensional vectors into high dimensional binary codes, to reduce storage complexity. In this approach, we deviate from adopting traditional hyperplane hashing functions and instead learn hyperspherical hashing functions. The proposed method overcomes the computational challenges of directly applying the spherical hashing algorithm that is intractable for compressing high dimensional vectors. A practical hierarchical model that utilizes divide and conquer techniques using the Random Select and Adjust (RSA) procedure to compress such high dimensional vectors is presented. We show that our proposed high dimensional binary codes outperform the binary codes obtained using traditional hyperplane methods for higher compression ratios. In the last part of the thesis, we propose a retrieval based solution to the Zero shot event classification problem - a setting where no training videos are available for the event. To do this, we learn a generic set of concept detectors and represent both videos and query events in the concept space. We then compute similarity between the query event and the video in the concept space and videos similar to the query event are classified as the videos belonging to the event. We show that we significantly boost the performance using concept features from other modalities.

Connecting the dots: Examining the role of parental beliefs and preschoolers’ affect and engagement in predicting parent-child number exploration during a meaningful math experience

The current study examined the frequency and quality of how 3- to 4-year-old children and their parents explore the relations between symbolic and non-symbolic quantities in the context of a playful math experience, as well as the role of both parent and child factors in this exploration. Preschool children’s numerical knowledge was assessed while parents completed a survey about the number-related experiences they share with their children at home, and their math-related beliefs. Parent-child dyads were then videotaped playing a modified version of the card game War. Results suggest that parents and children explored quantity explicitly on only half of the cards and card pairs played, and dyads of young children and those with lower number knowledge tended to be most explicit in their quantity exploration. Dyads with older children, on the other hand, often completed their turns without discussing the numbers at all, likely because they were knowledgeable enough about numbers that they could move through the game with ease. However, when dyads did explore the quantities explicitly, they focused on identifying numbers symbolically, used non-symbolic card information interchangeably with symbolic information to make the quantity comparison judgments, and in some instances, emphasized the connection between the symbolic and non-symbolic number representations on the cards. Parents reported that math experiences such as card game play and quantity comparison occurred relatively infrequently at home compared to activities geared towards more foundational practice of number, such as counting out loud and naming numbers. However, parental beliefs were important in predicting both the frequency of at-home math engagement as well as the quality of these experiences. In particular, parents’ specific beliefs about their children’s abilities and interests were associated with the frequency of home math activities, while parents’ math-related ability beliefs and values along with children’s engagement in the card game were associated with the quality of dyads’ number exploration during the card game. Taken together, these findings suggest that card games can be an engaging context for parent-preschooler exploration of numbers in multiple representations, and suggests that parents’ beliefs and children’s level of engagement are important predictors of this exploration.