Computer Sciences Commons^™

From Boolean Equalities To Constraints, Sergio Antoy, Michael Hanus

Computer Science Faculty Publications and Presentations

Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction …

The Performance Of Random Prototypes In Hierarchical Models Of Vision, Kendall Lee Stewart

Dissertations and Theses

I investigate properties of HMAX, a computational model of hierarchical processing in the primate visual cortex. High-level cortical neurons have been shown to respond highly to particular natural shapes, such as faces. HMAX models this property with a dictionary of natural shapes, called prototypes, that respond to the presence of those shapes. The resulting set of similarity measurements is an effective descriptor for classifying images. Curiously, prior work has shown that replacing the dictionary of natural shapes with entirely random prototypes has little impact on classification performance. This work explores that phenomenon by studying the performance of random prototypes on …

Prediction: The Quintessential Model Validation Test, Wayne Wakeland

Systems Science Friday Noon Seminar Series

It is essential to objectively test how well policy models predict real world behavior. The method used to support this assertion involves the review of three SD policy models emphasizing the degree to which the model was able to fit the historical outcome data and how well model-predicted outcomes matched real world outcomes as they unfolded. Findings indicate that while historical model agreement is a favorable indication of model validity, the act of making predictions without knowing the actual data, and comparing these predictions to actual data, can reveal model weaknesses that might be overlooked when all of the available …

A Constraint Language For Static Semantic Analysis Based On Scope Graphs, Hendrik Van Antwerpen, Pierre Néron, Andrew Tolmach, Eelco Visser, Guido Wachsmuth

Computer Science Faculty Publications and Presentations

In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs—such as record field access—for which binding and typing are mutually dependent.We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for …

Evaluation Of Data-Path Topologies For Self-Timed Conditional Statements, Navaneeth Prasannakumar Jamadagni

Dissertations and Theses

This research presents a methodology to evaluate data path topologies that implement a conditional statement for an average-case performance that is better than the worst-case performance. A conditional statement executes one of many alternatives depending on how Boolean conditions evaluate to true or false. Alternatives with simple computations take less time to execute. The self-timed designs can exploit the faster executing alternatives and provide an average-case behavior, where the average depends on the frequency of simple and complex computations, and the difference in the completion times of simple and complex computations. The frequency of simple and complex computations depends on …

Tweakable Ciphers: Constructions And Applications, Robert Seth Terashima

Dissertations and Theses

Tweakable ciphers are a building block used to construct a variety of cryptographic algorithms. Typically, one proves (via a reduction) that a tweakable-cipher-based algorithm is about as secure as the underlying tweakable cipher. Hence improving the security or performance of tweakable ciphers immediately provides corresponding benefits to the wide array of cryptographic algorithms that employ them. We introduce new tweakable ciphers, some of which have better security and others of which have better performance than previous designs. Moreover, we demonstrate that tweakable ciphers can be used directly (as opposed to as a building block) to provide authenticated encryption with associated …

Scalable Equivalence Checking For Behavioral Synthesis, Zhenkun Yang

Dissertations and Theses

Behavioral synthesis is the process of compiling an Electronic System Level (ESL) design to a register-transfer level (RTL) implementation. ESL specifications define the design functionality at a high level of abstraction (e.g., with C/C++ or SystemC), and thus provide a promising approach to address the exacting demands to develop feature-rich, optimized, and complex hardware systems within aggressive time-to-market schedules. Behavioral synthesis entails application of complex and error-prone transformations during the compilation process. Therefore, the adoption of behavioral synthesis highly depends on our ability to ensure that the synthesized RTL conforms to the ESL description. This dissertation provides an end-to-end scalable …

A Scaffolded, Metamorphic Ctf For Reverse Engineering, Wu-Chang Feng

Computer Science Faculty Publications and Presentations

Hands-on Capture-the-Flag (CTF) challenges tap into and cultivate the intrinsic motivation within people to solve puzzles, much in the same way Sudoku and crossword puzzles do. While the format has been successful in security competitions, there have been a limited number of attempts to integrate them into a classroom environment. This paper describes MetaCTF, a metamorphic set of CTF challenges for teaching reverse code engineering. MetaCTF is 1) scaffolded in a way that allows students to make incremental progress, 2) integrated with the course material so that students can immediately apply knowledge gained in class, 3) polymorphic and metamorphic so …

Reinforced Imitative Graph Learning For Mobile User Profiling, Dongjie Wang, Pengyang Wang, Yanjie Fu, Kunpeng Liu, Hui Xiong, Charles Hughes

Computer Science Faculty Publications and Presentations

Mobile user profiling refers to the efforts of extracting users’ characteristics from mobile activities. In order to capture the dynamic varying of user characteristics for generating effective user profiling, we propose an imitation-based mobile user profiling framework. Considering the objective of teaching an autonomous agent to imitate user mobility based on the user’s profile, the user profile is the most accurate when the agent can perfectly mimic the user behavior patterns. The profiling framework is formulated into a reinforcement learning task, where an agent is a next-visit planner, an action is a POI that a user will visit next, and …

Novel Cryptographic Primitives And Protocols For Censorship Resistance, Kevin Patrick Dyer

Dissertations and Theses

Internet users rely on the availability of websites and digital services to engage in political discussions, report on newsworthy events in real-time, watch videos, etc. However, sometimes those who control networks, such as governments, censor certain websites, block specific applications or throttle encrypted traffic. Understandably, when users are faced with egregious censorship, where certain websites or applications are banned, they seek reliable and efficient means to circumvent such blocks. This tension is evident in countries such as a Iran and China, where the Internet censorship infrastructure is pervasive and continues to increase in scope and effectiveness.

An arms race is …

Compiling Collapsing Rules In Certain Constructor Systems, Sergio Antoy, Andy Jost

Computer Science Faculty Publications and Presentations

The implementation of functional logic languages by means of graph rewriting requires a special handling of collapsing rules. Recent advances about the notion of a needed step in some constructor systems offer a new approach to this problem. We present two results: a transformation of a certain class of constructor-based rewrite systems that eliminates collapsing rules, and a rewrite-like relation that takes advantage of the absence of collapsing rules. We formally state and prove the correctness of these results. When used together, these results simplify without any loss of efficiency an implementation of graph rewriting and consequently of functional logic …

Automatic Fault Injection For Driver Robustness Testing, Kai Cong, Li Lei, Zhenkun Yang, Fei Xie

Computer Science Faculty Publications and Presentations

Robustness testing is a crucial stage in the device driver development cycle. To accelerate driver robustness testing, effective fault scenarios need to be generated and injected without requiring much time and human effort. In this pa- per, we present a practical approach to automatic runtime generation and injection of fault scenarios for driver robust- ness testing. We identify target functions that can fail from runtime execution traces, generate effective fault scenarios on these target functions using a bounded trace-based it- erative strategy, and inject the generated fault scenarios at runtime to test driver robustness using a permutation-based injection mechanism. We …

Exploratory Data Modeling Of Traumatic Brain Injury, Martin Zwick

Systems Science Faculty Publications and Presentations

A short presentation of an analysis of data from Dr. Megan Preece on traumatic brain injury, the first in a series of planned secondary analyses of multiple TBI data sets. The analysis employs the systems methodology of reconstructability analysis (RA), utilizing both variable- and state-based and both neutral and directed models. The presentation explains RA and illustrates the results it can obtain. Unlike the confirmatory approach standard to most data analyses, this methodology is designed for exploratory modeling. It thus allows the discovery of unanticipated associations among variables, including multi-variable interaction effects of unknown form. It offers the opportunity for …

Post-Silicon Functional Validation With Virtual Prototypes, Kai Cong

Dissertations and Theses

Post-silicon validation has become a critical stage in the system-on-chip (SoC) development cycle, driven by increasing design complexity, higher level of integration and decreasing time-to-market. According to recent reports, post-silicon validation effort comprises more than 50% of the overall development effort of an 65nm SoC. Though post-silicon validation covers many aspects ranging from electronic properties of hardware to performance and power consumption of whole systems, a central task remains validating functional correctness of both hardware and its integration with software. There are several key challenges to achieving accelerated and low-cost post-silicon functional validation. First, there is only limited silicon observability …

Hardware/Software Interface Assurance With Conformance Checking, Li Lei

Dissertations and Theses

Hardware/Software (HW/SW) interfaces are pervasive in modern computer systems. Most of HW/SW interfaces are implemented by devices and their device drivers. Unfortunately, HW/SW interfaces are unreliable and insecure due to their intrinsic complexity and error-prone nature. Moreover, assuring HW/SW interface reliability and security is challenging. First, at the post-silicon validation stage, HW/SW integration validation is largely an ad-hoc and time-consuming process. Second, at the system deployment stage, transient hardware failures and malicious attacks make HW/SW interfaces vulnerable even after intensive testing and validation. In this dissertation, we present a comprehensive solution for HW/SW interface assurance over the system life cycle. …

Novel Methods For Learning And Adaptation In Chemical Reaction Networks, Peter Banda

Dissertations and Theses

State-of-the-art biochemical systems for medical applications and chemical computing are application-specific and cannot be re-programmed or trained once fabricated. The implementation of adaptive biochemical systems that would offer flexibility through programmability and autonomous adaptation faces major challenges because of the large number of required chemical species as well as the timing-sensitive feedback loops required for learning. Currently, biochemistry lacks a systems vision on how the user-level programming interface and abstraction with a subsequent translation to chemistry should look like. By developing adaptation in chemistry, we could replace multiple hard-wired systems with a single programmable template that can be (re)trained to …

Non-Orientable Objects As Gaming Surfaces, Haley P. Bourke, Paul Latiolais

Student Research Symposium

Developed in Python, Klein Space Fighter is an interactive learning tool and mathematically themed arcade game that allows the player to combat on different mathematical surfaces including a 2D Klein bottle. The app is available for Android and desktop devices, and will be made available for iOS in the future.

To receive an invitation to download the app through Google Play, contact me at HaleyoBourke@yahoo.com

Naturalized Communication And Testing, Marly Roncken, Swetha Mettala Gilla, Hoon Park, Navaneeth Prasannakumar Jamadagni, Christopher Cowan, Ivan Sutherland

Computer Science Faculty Publications and Presentations

We ”naturalize” the handshake communication links of a self-timed system by assigning the capabilities of filling and draining a link and of storing its full or empty status to the link itself. This contrasts with assigning these capabilities to the joints, the modules connected by the links, as was previously done. Under naturalized communication, the differences between Micropipeline, GasP, Mousetrap, and Click circuits are seen only in the links — the joints become identical; past, present, and future link and joint designs become interchangeable. We also “naturalize” the actions of a self-timed system, giving actions status equal to states — …

Micro-Policies: Formally Verified, Tag-Based Security Monitors, Arthur Azevedo De Amorim, Maxime Denes, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach

Computer Science Faculty Publications and Presentations

Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies (or micro-policies) to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level “symbolic machine,” and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy’s rules embodies a high-level …

Intersections Of Critical Systems Thinking And Community Based Participatory Research In Developing A Web Site For Autistic Adults, Dora Madeline Raymaker

Dissertations and Theses

People with disabilities, including those on the autism spectrum, comprise the world's largest minority and experience significant inequities in Internet use. Existing standards for accessible web sites are necessary but not sufficient without the direct engagement of end users in identifying access needs. Yet little is known about methods for effective engagement, and there are no systematically derived Web accessibility guidelines for autistic end users. Here I explore a hybrid approach to direct engagement using critical systems thinking (CST) and community based participatory research (CBPR) during the co-development of a healthcare-focused web site by the Academic Autism Spectrum Partnership in …

Leveraging Contextual Relationships Between Objects For Localization, Clinton Leif Olson

Dissertations and Theses

Object localization is currently an active area of research in computer vision. The object localization task is to identify all locations of an object class within an image by drawing a bounding box around objects that are instances of that class. Object locations are typically found by computing a classification score over a small window at multiple locations in the image, based on some chosen criteria, and choosing the highest scoring windows as the object bounding-boxes. Localization methods vary widely, but there is a growing trend towards methods that are able to make localization more accurate and efficient through the …

Delay Line As A Chemical Reaction Network, Josh Moles, Peter Banda, Christof Teuscher

Computer Science Faculty Publications and Presentations

Chemistry as an unconventional computing medium presently lacks a systematic approach to gather, store, and sort data over time. To build more complicated systems in chemistries, the ability to look at data in the past would be a valuable tool to perform complex calculations. In this paper we present the first implementation of a chemical delay line providing information storage in a chemistry that can reliably capture information over an extended period of time. The delay line is capable of parallel operations in a single instruction, multiple data (SIMD) fashion.

Using Michaelis-Menten kinetics, we describe the chemical delay line implementation …

Semi-Modular Delay Model Revisited In Context Of Relative Timing, Hoon Park, Anping He, Marly Roncken, Xiaoyu Song

Electrical and Computer Engineering Faculty Publications and Presentations

A new definition of semi-modularity to accommodate relative timing constraints in self-timed circuits is presented. While previous definitions ignore such constraints, the new definition takes them into account. The difference on a design solution for a well-known speed-independent circuit implementation of the Muller C element and a set of relative timing constraints that renders the implementation hazard free is illustrated. The old definition produces a false semi-modularity conflict that cannot exist due to the set of imposed constraints. The new definition correctly accepts the solution.

Static Conflict Detection For A Policy Language, Alix Trou, Robert Dockins, Andrew Tolmach

Computer Science Faculty Publications and Presentations

We present a static control flow analysis used in the Simple Unified Policy Programming Language (SUPPL) compiler to detect internally inconsistent policies. For example, an access control policy can decide to both “allow” and “deny” access for a user; such an inconsistency is called a conflict. Policies in Suppl. follow the Event-Condition-Action paradigm; predicates are used to model conditions and event handlers are written in an imperative way. The analysis is twofold; it first computes a superset of all conflicts by looking for a combination of actions in the event handlers that might violate a user-supplied definition of conflicts. SMT …

Needed Computations Shortcutting Needed Steps, Sergio Antoy, Jacob Johannsen, Steven Libby

Computer Science Faculty Publications and Presentations

We define a compilation scheme for a constructor-based, strongly-sequential, graph rewriting system which shortcuts some needed steps. The object code is another constructor-based graph rewriting system. This system is normalizing for the original system when using an innermost strategy. Consequently, the object code can be easily implemented by eager functions in a variety of programming languages. We modify this object code in a way that avoids total or partial construction of the contracta of some needed steps of a computation. When computing normal forms in this way, both memory consumption and execution time are reduced compared to ordinary rewriting computations …

Ear-Phone: A Context-Aware Noise Mapping Using Smart Phones, Rajib Rana, Chun Tung Chou, Nirupama Bulusu, Salil Kanhere, Wen Hu

Computer Science Faculty Publications and Presentations

A noise map facilitates the monitoring of environmental noise pollution in urban areas. It can raise citizen awareness of noise pollution levels, and aid in the development of mitigation strategies to cope with the adverse effects. However, state-of-the-art techniques for rendering noise maps in urban areas are expensive and rarely updated (for months or even years), as they rely on population and traffic models rather than on real data. Smart phone based urban sensing can be leveraged to create an open and inexpensive platform for rendering up-to-date noise maps. In this paper, we present the design, implementation and performance evaluation …

S-Store: Streaming Meets Transaction Processing, John Meehan, Nesime Tatbul, Cansu Aslantas, Ugur Cetintemel, Jiang Du, Tim Kraska, Samuel Madden, David Maier, Andrew Pavlo, Michael Stonebraker, Kristin A. Tufte, Hao Wang

Computer Science Faculty Publications and Presentations

Stream processing addresses the needs of real-time applications. Transaction processing addresses the coordination and safety of short atomic computations. Heretofore, these two modes of operation existed in separate, stove-piped systems. In this work, we attempt to fuse the two computational paradigms in a single system called S-Store. In this way, S-Store can simultaneously accommodate OLTP and streaming applications. We present a simple transaction model for streams that integrates seamlessly with a traditional OLTP system. We chose to build S-Store as an extension of H-Store, an open-source, in-memory, distributed OLTP database system. By implementing S-Store in this way, we can make …

A Theory Of Name Resolution, Pierre Néron, Andrew Tolmach, Eelco Visser, Guido Wachsmuth

Computer Science Faculty Publications and Presentations

We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and language- independent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we …

Usage Based Topology For Dcns, Qing Yi, Suresh Singh

Computer Science Faculty Publications and Presentations

Many data center network topologies are designed to provide full bisection bandwidth for tens of thousands of servers in order to achieve high network throughput and server agility. However, the utilization rate of DCNs on average is below 10%, which results in a significant waste of network resources and energy. Many researchers propose consolidating network traffic flows to maximize the set of idle network equipment and switching them to low power mode to save energy. In this paper, we propose using skinnier network topologies to meet performance requirements of realistic loads thus saving not only energy but capital cost as …

Desiderata For A Big Data Language, David Maier

Computer Science Faculty Publications and Presentations

Data management and analytics systems for big data have proliferated, including column stores, array databases, graphanalysis environments and linear-algebra packages. This burgeoning of systems has lead to a surfeit of language and APIs. It is time to consider a new framework that can span these systems and simplify the programming and maintenance of Big Data applications. There are two key goals for such a framework:

Portability: It should be relatively easy to move an application or tool developed on one platform to operate against another. As a corollary, back-end data and analytics services should be swappable in a particular …