Crowdsourcing platforms provide a common market place for job seekers and requesters to work collaboratively. The existing platforms fail to address the needs of the workers and the requesters due to unjust distribution of power and insufficient information about the parties involved in a task. In platforms such as Amazon Mechanical Turk new workers struggle to find tasks, workers face rejection without adequate feedback, whereas requesters do not get high quality results in time. In this research we contribute to Daemo a collaborative project from Stanford crowd research collective. Daemo is a self-governed crowdsourcing platform that aims to improve work quality and provide equitable representation. We studied the surrounding literature about existing solutions to learn about the flaws in the current platforms. Then, we interviewed professional workers and requesters to find their needs. We envisioned ways to improve the requester experience by suggesting tagging for tasks to make the tags easier to be searched and tailored for their skills. We also proposed adding ratings to requesters profile and adding rejection rate to requester profiles. Then, we illustrated our design choices by creating prototypes to communicate and evaluate our work.

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.

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.

Natural language is made up of many different sentences connected to form coherent discourse. Shallow discourse parsing is the method of parsing through a given text to find the discourse relationship between pairs of related ideas. For example, given the following text, "having just one firm do this isn't going to mean a hill of beans. But if this prompts others to consider the same thing, then it may become much more important", the word 'but' functions as a discourse connective and connects the two ideas together. In this project, we developed an end-to-end parser that takes English or Chinese news stories and locates all of the discourse relations in the text. Our system can identify both explicit and implicit connectives, the location of the text they connect, and the type of the connective. Nine separate classifiers are chained together to create the full system. The system has been entered into the CONLL 2016 shared task on shallow discourse parsing. Performance of our system was compared with performance of systems from several other universities. Currently, ideas in text can only be understood within a single sentence. We hope to match the state of the art performance in this task, 92% accuracy in identifying discourse relations of a typical news article. Developments in shallow discourse parsing are the first step in automatically connecting ideas across many sentences. Such developments have opened the door for applications in automatic information extraction, summarization, and question answering systems.

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.

Blind programmers bring a unique perspective to the computer developer workplace, and make important contributions to the computer science field. However, blind programmers often cannot use computer development environments because they are inaccessible, and usage can be slow and tedious for blind developers who use screen readers. The goal of our research is to design and build plug-ins for various coding environments to make it easier for blind developers to code. In prior work, Ms. Baker made a plug-in called StructJumper for Eclipse, a Java Integrated Development Environment (IDE). The plug-in creates a navigable hieratical tree based on the nesting structure of a Java class, essentially creating an outline of key points (such as method headings and control flow statements) in the code structure. Blind programmers can switch between StructJumper’s TreeView and default Text Editor to navigate code with greater ease. The usability of StructJumper was tested by seven blind programmers, whose results showed a trend of completing tasks faster with the plug-in then without. This suggests that StructJumper is a viable plug-in to improve accessibility to blind developers. However Java is not the only major programming language developers’ use on a daily basis. Thus we are pursuing further research to extend StructJumper beyond Java and implement plug-ins/add-ons for other commonly used programming languages and development environments, such as for the programming language Python. My work is the start of coding StructJumper as a plug-in for Visual Studio (practically the only screen reader compatible Python IDE). This plug-in is written in Visual Studio using C#, .NET framework, and IronPython to parse Python files open in the IDE.