Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Physical Sciences and Mathematics (122)
- Computer Sciences (115)
- Computer and Systems Architecture (77)
- Electrical and Computer Engineering (47)
- Digital Communications and Networking (34)
-
- OS and Networks (32)
- Robotics (22)
- Data Storage Systems (14)
- Systems Architecture (13)
- Digital Circuits (11)
- Social and Behavioral Sciences (9)
- Databases and Information Systems (6)
- Other Computer Engineering (6)
- Mechanical Engineering (5)
- Theory and Algorithms (5)
- Business (4)
- Electronic Devices and Semiconductor Manufacturing (4)
- Life Sciences (4)
- Physics (4)
- Software Engineering (4)
- Systems and Communications (4)
- Artificial Intelligence and Robotics (3)
- Communication (3)
- Economics (3)
- Engineering Education (3)
- Information Security (3)
- Operations Research, Systems Engineering and Industrial Engineering (3)
- Quantum Physics (3)
- Keyword
-
- Adaptive computing systems (18)
- Electronic data processing -- Distributed processing (15)
- Parallel processing (Electronic computers) (13)
- Streaming technology (Telecommunications) (13)
- Multimedia systems (12)
-
- Neural networks (Computer science) (12)
- Machine learning (9)
- Functional programming (Computer science) (8)
- Computer algorithms (6)
- Computer architecture (6)
- Computer architecture -- Design (6)
- Computer vision (6)
- Operating systems (Computers) -- Design and construction (6)
- Robotics (6)
- Artificial intelligence (5)
- Image processing -- Digital techniques (5)
- Operating systems (Computers) (5)
- Robots -- Motion (5)
- System analysis (5)
- Computer networks (4)
- Computer networks -- Security measures (4)
- Memory management (Computer science) (4)
- Multimedia systems - Design (4)
- Natural computation (4)
- Operating systems (Computers) -- Evaluation (4)
- Parallel computers (4)
- Robots -- Design and construction (4)
- Software architecture (4)
- Synchronization (4)
- Algorithms (3)
- Publication Year
- Publication
-
- Computer Science Faculty Publications and Presentations (110)
- Dissertations and Theses (74)
- Maseeh Summer Undergraduate Research Experience (21)
- Electrical and Computer Engineering Faculty Publications and Presentations (13)
- Complex Systems Faculty Publications and Presentations (11)
-
- Engineering and Technology Management Faculty Publications and Presentations (6)
- REU Final Reports (5)
- Student Research Symposium (5)
- University Honors Theses (4)
- altREU Projects (4)
- PSU High School Innovation Challenge (3)
- Civil and Environmental Engineering Faculty Publications and Presentations (2)
- Engineering and Technology Management Student Projects (1)
- Mathematics and Statistics Faculty Publications and Presentations (1)
- Mechanical and Materials Engineering Faculty Publications and Presentations (1)
- PDXPLORES Podcast (1)
- Systems Science Friday Noon Seminar Series (1)
- University Studies Faculty Publications and Presentations (1)
- Publication Type
Articles 91 - 120 of 264
Full-Text Articles in Computer Engineering
Fast On-Line Kernel Density Estimation For Active Object Localization, Anthony D. Rhodes, Max H. Quinn, Melanie Mitchell
Fast On-Line Kernel Density Estimation For Active Object Localization, Anthony D. Rhodes, Max H. Quinn, Melanie Mitchell
Computer Science Faculty Publications and Presentations
A major goal of computer vision is to enable computers to interpret visual situations—abstract concepts (e.g., “a person walking a dog,” “a crowd waiting for a bus,” “a picnic”) whose image instantiations are linked more by their common spatial and semantic structure than by low-level visual similarity. In this paper, we propose a novel method for prior learning and active object localization for this kind of knowledge-driven search in static images. In our system, prior situation knowledge is captured by a set of flexible, kernel-based density estimations— a situation model—that represent the expected spatial structure of the given situation. These …
Making Software, Making Regions: Labor Market Dualization, Segmentation, And Feminization In Austin, Portland And Seattle, Dillon Mahmoudi
Making Software, Making Regions: Labor Market Dualization, Segmentation, And Feminization In Austin, Portland And Seattle, Dillon Mahmoudi
Dissertations and Theses
Through mixed-methods research, this dissertation details the regionally variegated and place-specific software production processes in three second-tier US software regions. I focus on the relationship between different industrial, firm, and worker production configurations and broad-based economic development, prosperity, and inequality. I develop four main empirical findings.
First, I argue for a periodization of software production that tracks with changes in software laboring activity, software technologies, and wage-employment relationships. Through a GIS-based method, I use the IPUMS-USA to extensively measure the amount and type of software labor in industries across the US between 1970 and 2015. I map the uneven geography …
Sparse Coding On Stereo Video For Object Detection, Sheng Y. Lundquist, Melanie Mitchell, Garrett T. Kenyon
Sparse Coding On Stereo Video For Object Detection, Sheng Y. Lundquist, Melanie Mitchell, Garrett T. Kenyon
Computer Science Faculty Publications and Presentations
Deep Convolutional Neural Networks (DCNN) require millions of labeled training examples for image classification and object detection tasks, which restrict these models to domains where such a dataset is available. We explore the use of unsupervised sparse coding applied to stereo-video data to help alleviate the need for large amounts of labeled data. In this paper, we show that unsupervised sparse coding is able to learn disparity and motion sensitive basis functions when exposed to unlabeled stereo-video data. Additionally, we show that a DCNN that incorporates unsupervised learning exhibits better performance than fully supervised networks. Furthermore, finding a sparse representation …
Memcapacitive Devices In Logic And Crossbar Applications, Dat Tran, Christof Teuscher
Memcapacitive Devices In Logic And Crossbar Applications, Dat Tran, Christof Teuscher
Electrical and Computer Engineering Faculty Publications and Presentations
Over the last decade, memristive devices have been widely adopted in computing for various conventional and unconventional applications. While the integration density, memory property, and nonlinear characteristics have many benefits, reducing the energy consumption is limited by the resistive nature of the devices. Memcapacitors would address that limitation while still having all the benefits of memristors. Recent work has shown that with adjusted parameters during the fabrication process, a metal-oxide device can indeed exhibit a memcapacitive behavior. We introduce novel memcapacitive logic gates and memcapacitive crossbar classifiers as a proof of concept that such applications can outperform memristor-based architectures. The …
Shift-Symmetric Configurations In Two-Dimensional Cellular Automata: Irreversibility, Insolvability, And Enumeration, Peter Banda, John S. Caughman Iv, Martin Cenek, Christof Teuscher
Shift-Symmetric Configurations In Two-Dimensional Cellular Automata: Irreversibility, Insolvability, And Enumeration, Peter Banda, John S. Caughman Iv, Martin Cenek, Christof Teuscher
Mathematics and Statistics Faculty Publications and Presentations
The search for symmetry as an unusual yet profoundly appealing phenomenon, and the origin of regular, repeating configuration patterns have been for a long time a central focus of complexity science, and physics.
Here, we introduce group-theoretic concepts to identify and enumerate the symmetric inputs, which result in irreversible system behaviors with undesired effects on many computational tasks. The concept of so-called configuration shift-symmetry is applied on two-dimensional cellular automata as an ideal model of computation. The results show the universal insolvability of “non-symmetric” tasks regardless of the transition function. By using a compact enumeration formula and bounding the number …
Video Frame Interpolation Via Adaptive Convolution, Simon Niklaus, Long Mai, Feng Liu
Video Frame Interpolation Via Adaptive Convolution, Simon Niklaus, Long Mai, Feng Liu
Computer Science Faculty Publications and Presentations
Video frame interpolation typically involves two steps: motion estimation and pixel synthesis. Such a two-step approach heavily depends on the quality of motion estimation. This paper presents a robust video frame interpolation method that combines these two steps into a single process. Specifically, our method considers pixel synthesis for the interpolated frame as local convolution over two input frames. The convolution kernel captures both the local motion between the input frames and the coefficients for pixel synthesis. Our method employs a deep fully convolu- tional neural network to estimate a spatially-adaptive con- volution kernel for each pixel. This deep neural …
Bayesian Optimization For Refining Object Proposals, Anthony D. Rhodes, Jordan Witte, Melanie Mitchell, Bruno Jedynak
Bayesian Optimization For Refining Object Proposals, Anthony D. Rhodes, Jordan Witte, Melanie Mitchell, Bruno Jedynak
Computer Science Faculty Publications and Presentations
We develop a general-purpose algorithm using a Bayesian optimization framework for the efficient refinement of object proposals. While recent research has achieved substantial progress for object localization and related objectives in computer vision, current state-of-the-art object localization procedures are nevertheless encumbered by inefficiency and inaccuracy. We present a novel, computationally efficient method for refining inaccurate bounding-box proposals for a target object using Bayesian optimization. Offline, image features from a convolutional neural network are used to train a model to predict an object proposal’s offset distance from a target object. Online, this model is used in a Bayesian active search to …
Proving Non-Deterministic Computations In Agda, Sergio Antoy, Michael Hanus, Steven Libby
Proving Non-Deterministic Computations In Agda, Sergio Antoy, Michael Hanus, Steven Libby
Computer Science Faculty Publications and Presentations
We investigate proving properties of Curry programs using Agda. First, we address the functional correctness of Curry functions that, apart from some syntactic and semantic differences, are in the intersection of the two languages. Second, we use Agda to model non-deterministic functions with two distinct and competitive approaches incorporating the non-determinism. The first approach eliminates non-determinism by considering the set of all non-deterministic values produced by an application. The second approach encodes every non-deterministic choice that the application could perform. We consider our initial experiment a success. Although proving properties of programs is a notoriously difficult task, the functional logic …
Cyberpdx: A Camp For Broadening Participation In Cybersecurity, Wu-Chang Feng, Robert Liebman, Lois Delcambre, Michael Mooradian Lupro, Tim Sheard, Scott Britell, Gerald W. Recktenwald
Cyberpdx: A Camp For Broadening Participation In Cybersecurity, Wu-Chang Feng, Robert Liebman, Lois Delcambre, Michael Mooradian Lupro, Tim Sheard, Scott Britell, Gerald W. Recktenwald
University Studies Faculty Publications and Presentations
With society’s increasing dependence on technology infrastructure, the importance of securing the computers, networks, data, and algorithms that run our digital and physical lives is becoming critical. To equip the next generation of citizens for the challenges ahead, an effort is underway to introduce security content early in a student’s academic career. It is important that these efforts broaden participation and increase diversity in the field. While many camps and curricula focus on introducing technical content and skills related to cybersecurity, such approaches can prematurely limit how students view career opportunities in the field, potentially limiting those who ultimately pursue …
An Inductive Ethnographic Study In Elderly Woman Technology Adoption And The Role Of Her Children, Noshad Rahimi, Antonie J, Jetter, Charles M. Weber
An Inductive Ethnographic Study In Elderly Woman Technology Adoption And The Role Of Her Children, Noshad Rahimi, Antonie J, Jetter, Charles M. Weber
Engineering and Technology Management Faculty Publications and Presentations
Elderly woman strives to have a streamlined life surrounded by ease and familiarity. As she is aging, her desire for simplicity grows, her self-efficacy weakens, her prudency intensifies and her overall inclination toward status quo strengthens. As a result, she delays, or refuses, making any decision that might bring complexity and disrupt the continuity in her life, particularly new and unfamiliar technologies (which often bring complexity, before providing ease). Consequently, her technology adoption has a much lower rate than that of other demographics. To open the black box of elderly woman technology adoption process, this study focuses on the role …
Vision-Based Motion For A Humanoid Robot, Khalid Abdullah Alkhulayfi
Vision-Based Motion For A Humanoid Robot, Khalid Abdullah Alkhulayfi
Dissertations and Theses
The overall objective of this thesis is to build an integrated, inexpensive, human-sized humanoid robot from scratch that looks and behaves like a human. More specifically, my goal is to build an android robot called Marie Curie robot that can act like a human actor in the Portland Cyber Theater in the play Quantum Debate with a known script of every robot behavior. In order to achieve this goal, the humanoid robot need to has degrees of freedom (DOF) similar to human DOFs. Each part of the Curie robot was built to achieve the goal of building a complete humanoid …
Factors Affecting Big Data Technology Adoption, Nayem Rahman
Factors Affecting Big Data Technology Adoption, Nayem Rahman
Student Research Symposium
With the advancement of computer science, hardware and software engineering, and computing power, and later with the advent of the internet, social networking tools and other sources such as sensors data growth has increased significantly. These data are called big data which are mostly unstructured, generated in large volumes, data need to be captured in near real-time. To handle big data a completely new set of tools and technologies are being emerged. I have studied big data literature to identify the factors that might influence big data adoption. I was able to list quite a few factors or attributes that …
A Backend Framework For The Efficient Management Of Power System Measurements, Benjamin Mccamish, Rich Meier, Jordan Landford, Robert B. Bass, David Chiu, Eduardo Cotilla-Sanchez
A Backend Framework For The Efficient Management Of Power System Measurements, Benjamin Mccamish, Rich Meier, Jordan Landford, Robert B. Bass, David Chiu, Eduardo Cotilla-Sanchez
Electrical and Computer Engineering Faculty Publications and Presentations
Increased adoption and deployment of phasor measurement units (PMU) has provided valuable fine-grained data over the grid. Analysis over these data can provide insight into the health of the grid, thereby improving control over operations. Realizing this data-driven control, however, requires validating, processing and storing massive amounts of PMU data. This paper describes a PMU data management system that supports input from multiple PMU data streams, features an event-detection algorithm, and provides an efficient method for retrieving archival data. The event-detection algorithm rapidly correlates multiple PMU data streams, providing details on events occurring within the power system. The event-detection algorithm …
Information Representation And Computation Of Spike Trains In Reservoir Computing Systems With Spiking Neurons And Analog Neurons, Amin Almassian
Information Representation And Computation Of Spike Trains In Reservoir Computing Systems With Spiking Neurons And Analog Neurons, Amin Almassian
Dissertations and Theses
Real-time processing of space-and-time-variant signals is imperative for perception and real-world problem-solving. In the brain, spatio-temporal stimuli are converted into spike trains by sensory neurons and projected to the neurons in subcortical and cortical layers for further processing.
Reservoir Computing (RC) is a neural computation paradigm that is inspired by cortical Neural Networks (NN). It is promising for real-time, on-line computation of spatio-temporal signals. An RC system incorporates a Recurrent Neural Network (RNN) called reservoir, the state of which is changed by a trajectory of perturbations caused by a spatio-temporal input sequence. A trained, non- recurrent, linear readout-layer interprets the …
Incorporating Priors For Medical Image Segmentation Using A Genetic Algorithm, Payel Ghosh, Melanie Mitchell, James A. Tanyi, Arthur Y. Hung
Incorporating Priors For Medical Image Segmentation Using A Genetic Algorithm, Payel Ghosh, Melanie Mitchell, James A. Tanyi, Arthur Y. Hung
Computer Science Faculty Publications and Presentations
Medical image segmentation is typically performed manually by a physician to delineate gross tumor volumes for treatment planning and diagnosis. Manual segmentation is performed by medical experts using prior knowledge of organ shapes and locations but is prone to reader subjectivity and inconsistency. Automating the process is challenging due to poor tissue contrast and ill-defined organ/tissue boundaries in medical images. This paper presents a genetic algorithm for combining representations of learned information such as known shapes, regional properties and relative position of objects into a single framework to perform automated three-dimensional segmentation. The algorithm has been tested for prostate segmentation …
A Verified Information-Flow Architecture, Arthur Azevedo De Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
A Verified Information-Flow Architecture, Arthur Azevedo De Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
Computer Science Faculty Publications and Presentations
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model. We …
Sparse Encoding Of Binocular Images For Depth Inference, Sheng Y. Lundquist, Dylan M. Paiton, Peter F. Schultz, Garrett T. Kenyon
Sparse Encoding Of Binocular Images For Depth Inference, Sheng Y. Lundquist, Dylan M. Paiton, Peter F. Schultz, Garrett T. Kenyon
Computer Science Faculty Publications and Presentations
Sparse coding models have been widely used to decompose monocular images into linear combinations of small numbers of basis vectors drawn from an overcomplete set. However, little work has examined sparse coding in the context of stereopsis. In this paper, we demonstrate that sparse coding facilitates better depth inference with sparse activations than comparable feed-forward networks of the same size. This is likely due to the noise and redundancy of feed-forward activations, whereas sparse coding utilizes lateral competition to selectively encode image features within a narrow band of depths.
High-Performance Computing For Drought Prediction, Henry Cooney
High-Performance Computing For Drought Prediction, Henry Cooney
Maseeh Summer Undergraduate Research Experience
In recent decades, there has been considerable interest in using satellite soil moisture data to examine the global water-energy cycle and manage water resources. Current satellites are limited in their sensing depth, and can only directly measure top soil layers. Using a particle filter, this data may be fused with the output of a hydrologic simulation to improve simulation results, and characterize a hydrologic system at the watershed level. However, this approach increases computational requirements dramatically, and requires rethinking to accommodate data scaling and achieve good performance.
We present a detailed performance study of several alternative implementations of the hybrid …
Emerging Adaptive Architectures For Biomolecular Computation, Matthew Fleetwood
Emerging Adaptive Architectures For Biomolecular Computation, Matthew Fleetwood
Maseeh Summer Undergraduate Research Experience
The goal of this work is to explore applications of reservoir computing in biomolecular computation. Reservoir computing is a unique model for representing a mapping from one instance in time to a specific output. A neural network of randomly connected neurons is linked with a single output neuron or multiple output neurons. The output neurons are capable of mapping inputs to desired outputs using adaptable algorithms. This framework is investigated by using the Python programming language and object oriented design and programming. Neurons are created in programs by bundling information like input data and attributes of the network, which utilize …
Formal Modeling And Verification Of Delay-Insensitive Circuits, Hoon Park
Formal Modeling And Verification Of Delay-Insensitive Circuits, Hoon Park
Dissertations and Theses
Einstein's relativity theory tells us that the notion of simultaneity can only be approximated for events distributed over space. As a result, the use of asynchronous techniques is unavoidable in systems larger than a certain physical size. Traditional design techniques that use global clocks face this barrier of scale already within the space of a modern microprocessor chip. The most common response by the chip industry for overcoming this barrier is to use Globally Asynchronous Locally Synchronous (GALS) design techniques. The circuits investigated in this thesis can be viewed as examples of GALS design. To make such designs trustworthy it …
From Boolean Equalities To Constraints, Sergio Antoy, Michael Hanus
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 …
Computational Capacity And Energy Consumption Of Complex Resistive Switch Networks, Jens Bürger, Alireza Goudarzi, Darko Stefanovic, Christof Teuscher
Computational Capacity And Energy Consumption Of Complex Resistive Switch Networks, Jens Bürger, Alireza Goudarzi, Darko Stefanovic, Christof Teuscher
Electrical and Computer Engineering Faculty Publications and Presentations
Resistive switches are a class of emerging nanoelectronics devices that exhibit a wide variety of switching characteristics closely resembling behaviors of biological synapses. Assembled into random networks, such resistive switches produce emerging behaviors far more complex than that of individual devices. This was previously demonstrated in simulations that exploit information processing within these random networks to solve tasks that require nonlinear computation as well as memory. Physical assemblies of such networks manifest complex spatial structures and basic processing capabilities often related to biologically-inspired computing. We model and simulate random resistive switch networks and analyze their computational capacities. We provide a …
Network Structure, Network Flows And The Phenomenon Of Influence In Online Social Networks: An Exploratory Empirical Study Of Twitter Conversations About Youtube Product Categories, Nitin Venkat Mayande
Network Structure, Network Flows And The Phenomenon Of Influence In Online Social Networks: An Exploratory Empirical Study Of Twitter Conversations About Youtube Product Categories, Nitin Venkat Mayande
Dissertations and Theses
Traditional marketing models are swiftly being upended by the advent of online social networks. Yet, practicing firms that are engaging with online social networks neither have a reliable theory nor sufficient practical experience to make sense of the phenomenon. Extant theory in particular is based on observations of the real world, and may thus not apply to online social networks. Practicing firms may consequently be misallocating a large amount of resources, simply because they do not know how the online social networks with which they interact are organized.
The purpose of this dissertation is to investigate how online social networks …
A Scaffolded, Metamorphic Ctf For Reverse Engineering, Wu-Chang Feng
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 …
Compiling Collapsing Rules In Certain Constructor Systems, Sergio Antoy, Andy Jost
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
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 …
Naturalized Communication And Testing, Marly Roncken, Swetha Mettala Gilla, Hoon Park, Navaneeth Prasannakumar Jamadagni, Christopher Cowan, Ivan Sutherland
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
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 …
A Study Of Microwave Curing Of Underfill Using Open And Closed Microwave Ovens, Aditya Thakare
A Study Of Microwave Curing Of Underfill Using Open And Closed Microwave Ovens, Aditya Thakare
Dissertations and Theses
As the demand for microprocessors is increasing with more and more consumers using integrated circuits in their daily life, the demand on the industry is increasing to ramp up production.
In order to speed up the manufacturing processes, new and novel approaches are trying to change certain aspects of it. Microwaves have been tried as an alternative to conventional ovens in the curing of the polymers used as underfills and encapsulants in integrated circuits packages. Microwaves however being electromagnetic waves have non uniform energy distribution in different settings, causing burning or incomplete cure of polymers.
In this study, we compare …
Semi-Modular Delay Model Revisited In Context Of Relative Timing, Hoon Park, Anping He, Marly Roncken, Xiaoyu Song
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.