Transcranial magnetic stimulation (TMS) is a method of noninvasively and reversibly influencing brain activity through the generation of brief magnetic fields. Utilizing this approach, we investigate the role of the semantic representation of objects in the dorsal portion of the premotor cortex (PMd). The ventral portion of the premotor cortex (PMv) has been known to be involved in the representation of manipulable objects, such as tools. Conversely, we provide evidence that stimulation of PMd facilitates access to foot-related objects (such as sandals or slippers) by observing decreased decision times in a categorization task when PMd is stimulated at 110% of motor threshold. Within this task, subjects are shown a category, either “object” or “animal”, and asked to select which of two options match the provided category. These findings also provide support for the notion that the human premotor cortex has a topological organization and that part of the organization of sematic knowledge for objects depends on the modality with which they are interacted.

Third-party content on websites (such as included advertisements or social media widgets) has recently become a huge topic in computer privacy and security, but few studies have examined the visual impact of third-party content on web pages. Without this information, developers of commonly used tools that interact with third-party content (such as AdBlock and Ghostery) are unable to provide users with information on which advertisers are responsible for specific pieces of content on the page, which users could then use to selectively block certain third parties responsible for undesirable content. This project, in contrast, focuses on the visual nature of different types of third-party content. To gather this information, I created a tool to detect when third-party content is inserted into web pages, allowing me to connect third-party content to DOM nodes (elements of a webpage). This correspondence allows me to collect information on the visual characteristics of elements inserted by various third parties after they have been rendered by the browser. I am able to gather information that Ghostery and AdBlock cannot collect because of their usage of network requests to identify third-party content. I use this information to survey the distribution of size and location of different third-party elements, comparing web pages from different categories and countries to uncover trends in the layout of third-party content. Preliminary results indicate that there are specific visual hotspots for third-party content, and there are a few domains that provide a disproportionate amount of visible third-party content. Other possible directions to explore with this information include improving current tools to help users make informed decisions about which third-parties to block or allow, helping developers debug their web pages, and giving the research community a deeper understanding of how third-party content affects the visual layout of web pages.

Transformations over assembly code are common in many compilers. Such transformations are useful in applications ranging from peephole optimizations to software fault isolation. These transformations are also some of the most bug-dense compiler components. Such bugs could be eliminated by formally verifying the compiler, but state of-the-art formally verified compilers like CompCert do not support assembly-level program transformations. This paper presents Peek, a framework for expressing, verifying, and running assembly-level program transformations in CompCert. Peek contributes four new components: a lower level semantics for CompCert x86 syntax, a liveness analysis, a library for expressing and verifying peephole optimizations, and a verified peephole optimization pass built into CompCert. Each of these is accompanied by a correctness proof in Coq against realistic assumptions about the calling convention and the system memory allocator. Verifying peephole optimizations in Peek requires proving only a set of local properties, which we have proved are sufficient to ensure global transformation correctness. We have proven these local properties for 26 peephole transformations from the literature. We discuss the development of our new assembly semantics, our liveness analysis, representation of program transformations, and execution engine, describe the verification challenges of each component, and detail techniques we applied to mitigate the proof burden.

We are investigating adverse event (AE) reporting in clinical trials on cystic fibrosis (CF) to address whether specific approaches to coding AEs prior to un-blinding of study data is informative. While attribution standards are available in the Common Toxicity Criteria; there are no formal guidelines on how this determination should be made. The process of reporting attributions increases both time and cost of the trial although it is uncertain whether this process is accurate or valuable. This is a retrospective data repeated measures data analysis with pooled clinical trial data from four randomized controlled trials involving patients with CF. We will employ descriptive statistics to describe the overall population and demographics from individual studies who experienced at least one adverse event and summarize the adverse event rates over all and per study by individual rates. We will also employ repeated multiple variable regression techniques to describe associations of demographic and clinical characteristics with the attribution of AE’s. We hypothesize that physicians are not very good at attributing these events when the patient is on the placebo. We currently have available data on 11,974 adverse events in 785 subjects in the four randomized controlled trials. This study could have implications to how clinical trials are conducted in the United States. A future goal would be to clarify the value of attribution of adverse events in clinical trials.

Sea ice plays a vital role in the Arctic ecosystem and is a good indicator of climate change, so it is important to understand the physical processes that control sea ice evolution in order to get a better sense of the detrimental effects of climate change on the environment. Thus, accurate measurements of the features of ice – such as ice concentration – are needed to provide a clearer picture of how and when the ice evolves. This project aims to document and quantify ice variability from airborne imagery during the summer melting season in the Beaufort Sea. Images were taken from US Coast Guard Arctic Domain Awareness (ADA) flights in June, July, August, and October of 2014, with data collection to be continued in coming summers, including this summer, the summer of 2015. Algorithms were developed to automate the identification and quantification of features of the sea ice and open water such as ice concentration, floe size, melt pond coverage, and melt pond size. This data will be charted over time and space (latitude) to identify and analyze patterns in the evolution of Arctic sea ice. Results from this study will be useful for verifying satellite data, evaluating models, and initializing predication schemes. This information will be helpful for quantifying and analyzing the effects of climate change on the Arctic ecosystem.

Phosphenes are temporary visual percepts which can be elicited via transcranial magnetic stimulation (TMS) of the visual cortex. Often described as flashes or blobs of light, phosphenes usually occupy a small subset of the visual field and can be consciously perceived and described by a human subject. In order to investigate the relationship between phosphene characteristics and the methods in which they are elicited, subjects were asked to draw the phosphenes they perceive in response to different stimulation intensities, locations, and orientations. This information was then used for direct brain-to-brain communication of simple images. Functional magnetic resonance imaging (fMRI) was utilized to decode information from the brain of one human (“the sender”) and TMS was used to encode that information into the brain of another human (“the receiver”). Namely, the image that the sender viewed was determined by monitoring oxygenated blood flow patterns in the brain and transmitted directly to the brain of the receiver. The receiver “saw” the image viewed by the sender through TMS-induced phosphenes which were elicited by stimulating with parameters determined during the mapping stage. This brain-to-brain interface allows for the successful transmission of complex visual information directly from one human brain to another and does so through noninvasive methods.

For my history thesis I am studying French intellectuals’ appropriation of World War II memory in debates over the Algerian war. My research involves close readings of the works of key French intellectuals, some of which were printed in major French periodicals like Le Monde, L’Express, and Les Temps modernes. I focus predominantly on the last Governor-General of Algeria Jacques Soustelle and philosopher Jean-Paul Sartre. In these intellectuals’ arguments, two opposing conceptions of national honor arise. Soustelle was a staunch supporter of French sovereignty in Algeria. He connected the war to France’s duty to combat totalitarian and tyrannical threats to democracy, embodied in his eyes in the FLN Algerian rebels. In contrast, Jean-Paul Sartre argued against the war and colonialism, disparaging France for resembling Germany during World War II and compromising its democratic values through the use of torture. Within the context of intellectual petitions and French military coup d’états, these opposing conceptions of honor polarized contemporary debates. These debates in turn contributed to an environment of political instability that brought about the fall of the Fourth French Republic in 1958 and pushed France to settle a cease-fire with the FLN in 1962. However, despite their differences, both Soustelle and Sartre’s conceptions of honor were rooted in the same democratic ideals of the French Resistance of World War II. My research thus also reveals the unique, powerful, yet also dangerous multiplicity of memory. Algerian war intellectual debates revealed that intellectuals could draw on the same collective memory of a previous conflict in order to support radically opposing contemporary arguments and agendas. This reminds us that contemporary conflicts and ensuing debates cannot be understood in a vacuum. Memory is a strong rhetorical tool, and in many ways must be considered central to political and historical scholarship.

Computers can produce undesired results when operating on large non-negative values. For example, a computer might compute (2^32 - 2) / (2^32 - 1) to be exactly 2, whereas the desired value is slightly less than 1. The computer representation of non-negative, or "unsigned", values is incompatible with the standard computer implementation of division for possibly negative, or "signed", values. If a programmer uses the wrong implementation of an operator, or mixes signed and unsigned values in a computation, that mistake can lead to incorrect calculations and even to security vulnerabilities. Our goal is to prevent such errors. To prevent introducing errors, programmers must segregate signed and unsigned values in their programs. This task is tedious and error-prone. We have built an automated tool that reports when a programmer has made a mistake related to signed and unsigned values. Even more importantly, the tool is sound: if the tool issues no warnings, then the program is guaranteed to contain no such errors. Our technical approach is called pluggable type-checking: it enriches the programming language's type system in order to represent signedness, which languages like Java do not currently handle. This approach is natural and easy-to-use for programmers. A programmer simply declares which values are unsigned, and our tool checks that these values are used soundly. Our implementation is publicly available as open-source at http://checkerframework.org/ . In case studies, it found a number of errors in real-world code. This illustrates the potential for our technique to make programming less error-prone and programs more reliable.

The web has become a pervasive part of our lives, giving us previously unfathomable access to information and computation. The dynamic, interactive experience of the modern web is made possible only by the substantial engineering efforts put into making web browsers run correctly and with high efficiency. Towards this aim, software engineers have crafted complex, highly specialized algorithms and tuned their performance largely through informal and experimental techniques. Web browser layout engines are a case in point; Google has 10 full-time staff members specifically dedicated to this component of Google Chrome. In our research, we set out to develop a system to transform a high-level description of such computations on a restricted domain of tree-shaped data structures into an algorithm to perform the computations on any input from this domain with both efficiency and correctness. More generally, this kind of transformation, involving the automated construction of a program from a high-level, constrained description, is known as program synthesis, or optimal program synthesis when optimization is incorporated into the process. In our case, we optimize with respect to the time necessary to compute or update a prior result based on a change in input by exploiting parallel and incremental computation. Existing, domain-specific implementations already incorporate both concepts but often suboptimally and sometimes even incorrectly, as they are notoriously difficult to get right. In our approach, we employ an automated theorem prover to perform multiple compositional searches over the space of candidate algorithms and select the optimal candidate according to our efficiency approximation methods. In the process of accomplishing this, we have created a novel approach to decomposing complex, almost intractable problems in program synthesis. Currently, we are applying this work to synthesize a highly performant web layout engine with guaranteed layout correctness.

Hand tracking algorithms take as input 2D or 3D images or videos of a hand and return the hand’s position or movement. Hand tracking has various applications from gesture recognition to gaming to sign language interpretation. The goal of my project is to build a robust hand tracker that uses a 3D camera. Given a 3D image from a depth camera, the algorithm must find the pose and joint values of the hand model. Some current methods for tracking a hand include particle filters, gradient descent on joint parameters, and convolutional neural networks (CNNs). Particle filters are the most accurate, but they are computationally expensive and are not real time. Gradient descent can be done in real time, but needs to be initialized and has a chance of losing track of the hand. Neural nets are able to detect a hand without initialization, but they typically suffer from inaccuracy. The approach I research combines a gradient descent method and a CNN to leverage the benefits of both frameworks. A set of 3D images get processed by a CNN, yielding estimates of the hand pose in each image. These estimates are then fed into a gradient descent optimizer to produce a final estimate for the pose. Results have shown that the neural network can successfully set an initial pose for the gradient descent method, after which the gradient descent improves the pose estimation over the neural network.

The use of mobile applications for real-time self monitoring of patients’ conditions has been growing rapidly in medical research and healthcare fields.  I am working with a team to build a smart aging monitoring mobile app, which will be particularly prototyped among participants of Seattle Longitudinal Study (SLS). Many of them are subject to the risk of developing aging diseases such as the Alzheimer’s disease (AD). AD is a degenerative disorder that can destroy memory and other important mental functions.  Currently there have been 5.3 million Americans suffering from AD, and with the demographic shift towards an aging society, this number is expected to double in the next decade. We feel a strong calling to build senior people monitoring tools to help them stay away from such disorders, as well a tool that assists monitoring and early intervention among AD patients. Therefore, we started our research project, named as “CHI - Contemporaneous Health Index for Smart Monitoring of Aging. CHI comprises of a smart mobile application for aging condition monitoring, evaluation, and health promotion and a series of machine learning algorithms that support these functions. In order to build the app, I researched and read related papers and resources about hte AD and form the related tasks and games for the patients in the app. I also researched and talked with my mentor to determine the types of body condition data to collect. The app also provides user with easy access to record their body condition readings. Users can also get their task results and our feedback. I conducted the app tests and make several test users to test and improve the app. In the future we will conduct various user tasks specifically designed for Alzheimer’s patients and we will collect user results by working with SLS for further analysis. It is anticipated to be a powerful tool that mainly focuses on monitoring, evaluating, and intervening the aging process, to characterize the “aging trajectory” of individuals, to identify abnormal patterns, and to further provide personalized recommendation that help users stay healthier, active and happy lives.

At full capacity, the University of Washington-Seattle Campus plays host to nearly thirty thousand undergraduates and fourteen thousand graduate and professional students. UW-Seattle provides an enormous amount of information to help students navigate over one hundred and eighty majors and degree programs. Lack of standardization and the diaspora of information across many department websites, however, makes it very difficult for students to effectively discover and plan course work, especially over their entire undergraduate or graduate career at the university. The Coursector Project seeks to address this disparity between the amount of information available for students and unfortunately complex nature of its structure: much of the information about courses and offerings is simply in text, with no visual aids or recommendation engines for students. By building web-ready data visualizations about course prerequisite relationships, the project allows students to see links between courses, majors, and areas of their interest. These interactive visualizations are made up of data scraped from the UW course catalog. Beyond using it for practical course planning purposes, students can also simply mess with the visualizations for fun, discovering new classes and course pathways they had not previously thought of. Furthermore, because of the interwoven nature of many interdisciplinary offerings at the University of Washington, many departments rely on one another for prerequisite courses and instruction. The data analysis and visualizations performed by the Coursector Project will also allow school administrators to address so called choke point classes: those which unlock access to many upper level classes in any given department. The data is all there. The Coursector Project helps students and staff alike make sense of it.

Clusters of rocket motors are classically arranged cylindrically for the purpose of maximizing the effective aerodynamics of the overall cross-sectional design. Alternatively, our team’s rocket booster engine configuration was arranged in a unique square formation around the main engine for the first stage of our launch. This not only simplified construction and reduced the need for extra material to support the engines, but also lent itself to increased stability by making use of the corners of the square as part of the fin design. This first stage consisted of nine identical motors ignited simultaneously. Once the second stage ignited, this nine-engine cluster detached from the rocket and propulsion continued via a single motor. Speeds reached approximately 550 m/s, which is to say approximately Mach 1.6. The mainframe was constructed of carbon fiber with Kevlar reinforcement to prevent the fins from self-destructing upon breaking the sound barrier and/or ground impact. Our payload consisted of electronics for measuring and transmitting acceleration, speed, and altitude, along with a GPS unit for tracking purposes. The rocket's objective was to reach 60K feet, the maximum altitude allowed by FAA regulations, with a supersonic square cluster design modeled after SpaceX’s Falcon9. The research conducted was to study the takeoff, flight stability, and landing of our rocket’s more efficient square orientation in comparison to a typical cylinder design.

In several studies regarding the history of colonialism, an analogy between female bodies and land has been made. Many scholars have discussed how an Empire exploits its colonies as well as sexually objectifies and claims ownership of colonial women. The main evidence of eroticization can be most manifestly observed in colonial dances among many other cultural phenomena, mainly due to the fundamental physicality of the art form. In this research, I aim to reveal how colonialism affected traditional dance forms of Hawaii and Korea, which had suffered from the rule of the United States and Japanese Empire for decades. Notable changes in the way female bodies were presented in Hawaiian Hula and Korean Shin-muyong (Korean neoclassical dance) are studied, as well as the trace of eroticization that still lives today. In order to identify characteristics of the colonial Hula and Shin-muyong, I shed new light on the lives of two most prominent Hawaiian Hula and Korean Shin-muyong dancers, Kini Kapahu and Choi Seung-hee. I draw on scholarship and archival resources indicating that they had one common strategy for success in the United States and Europe: colonial exhibition. Understanding of the power relation between colonial women and imperial audience of the time can be inferred from the literature analysis. In addition, I take warning against the undying specter of colonialism by illuminating how modern tourism sells the descendants of Kini Kapahu and Choi Seung-hee, or Hawaiian and Korean female dancers of the 21st century, as exotic commodities that satisfy the sexual aspiration of tourist conquerors.

As sensors decrease in size, cost, and power, more and more sensors are being used to generate big data sets – a concept called the “Internet of Things.’’ These data sets must be analyzed to extract meaningful information from it. Consequently, tools or techniques for analyzing large data sets from sensor networks are important. This idea of building a data pipeline for the Internet of Things is what our project is based on. The purpose of our research project was to construct a database to store distributed sensor network data and to enable analysis of the data. Sensor data consisted of information from devices that were connected to nearby wireless networks. The data were gathered using a low-cost and low-power microcomputers, in our case, Raspberry Pis, and were collected from the sensors over several days. These were stored in the database for analysis. The large-scale data sets that result make a database necessary for analysis. The concept of gathering big data sets from sensor networks and performing data analysis can be used in optimization, prediction, control, and other applications. Data pipelines also enable analysis at different time scales from data acquisition. Designing tools for our more data-rich world is essential to understanding the mass of data that we gather each day from the sensors all around us.

The principal technological problem of the renewable energy industry is how to supply energy at its rate of demand and at a marginal cost less than that of present energy storage systems. One of the greatest challenges of this problem is the necessity of storing a portion of total produced energy such that it can be used when the instantaneous rate of energy demand differs from the limits of its instantaneous rate of production to balance out the demand and supply for energy. Our research focuses on the storage problem of current Under Water Compressed Air Energy Storage (UW-CAES) systems; in particular on decreasing the costs and environmental impact of air storage by performing electrolysis in a deep-sea electrolyzer to capitalize on the extreme energy densities already-available at depth and increase the energy density of each storage vessel/balloon by storing both hydrogen and oxygen. We demonstrate a method that increases the efficiency of energy storage by performing electrolysis using the high pressures available at depth, thereby eliminating the use of costly compressors and create a condition for the apparatus to be as close to a thermo neutral state.