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.

Regular homomorphisms of minimal sets

The classification of minimal sets is a central theme in abstract topological dynamics. Recently this work has been strengthened and extended by consideration of homomorphisms. Background material is presented in Chapter I. Given a flow on a compact Hausdorff space, the action extends naturally to the space of closed subsets, taken with the Hausdorff topology. These hyperspaces are discussed and used to give a new characterization of almost periodic homomorphisms. Regular minimal sets may be described as minimal subsets of enveloping semigroups. Regular homomorphisms are defined in Chapter II by extending this notion to homomorphisms with minimal range. Several characterizations are obtained. In Chapter III, some additional results on homomorphisms are obtained by relativizing enveloping semigroup notions. In Veech's paper on point distal flows, hyperspaces are used to associate an almost one-to-one homomorphism with a given homomorphism of metric minimal sets. In Chapter IV, a non-metric generalization of this construction is studied in detail using the new notion of a highly proximal homomorphism. An abstract characterization is obtained, involving only the abstract properties of homomorphisms. A strengthened version of the Veech Structure Theorem for point distal flows is proved. In Chapter V, the work in the earlier chapters is applied to the study of homomorphisms for which the almost periodic elements of the associated hyperspace are all finite. In the metric case, this is equivalent to having at least one fiber finite. Strong results are obtained by first assuming regularity, and then assuming that the relative proximal relation is closed as well.

Place in Time: The Role of Architecture in Establishing an Emotional Connection between Man and Time

This thesis explores the role of architecture as a means of reconnecting humans to the passage of time. A neglect of the temporal in our built environment obscures understanding of the human condition in all of its sensory aspects. The exploration and design of a series of ritual engagements, both culturally, and architecturally, begin to offer a venue through which designers can engage human senses. Rituals act as a means of demarcating the passage of time. It is through the engagement with these moments that people can begin to gain a richer understanding of the ephemeral nature of their own existence. The Pritzker Architecture Prize serves as the selected ritual of exploration because of its celebration of humanity and the art of architecture. However, the notion of ritual is explored down to the level of detail of engagement with handrails and door handles.