Current Search: Jha, Sumit (x)
View All Items
(1 - 20 of 33)
Pages
- Title
- COMPUTATION OF BOOLEAN FORMULAS USING SNEAK PATHS IN CROSSBAR COMPUTING.
- Creator
-
Velasquez, Alvaro, Jha, Sumit, University of Central Florida
- Abstract / Description
-
Memristor-based nano-crossbar computing is a revolutionary computing paradigm that does away with the traditional Von Neumann architectural separation of memory and computation units. The computation of Boolean formulas using memristor circuits has been a subject of several recent investigations. Crossbar computing, in general, has also been a topic of active interest, but sneak paths have posed a hurdle in the design of pervasive general-purpose crossbar computing paradigms. In this paper,...
Show moreMemristor-based nano-crossbar computing is a revolutionary computing paradigm that does away with the traditional Von Neumann architectural separation of memory and computation units. The computation of Boolean formulas using memristor circuits has been a subject of several recent investigations. Crossbar computing, in general, has also been a topic of active interest, but sneak paths have posed a hurdle in the design of pervasive general-purpose crossbar computing paradigms. In this paper, we demonstrate that sneak paths in nano-crossbar computing can be exploited to design a Boolean-formula evaluation strategy. We demonstrate our approach on a simple Boolean formula and a 1-bit addition circuit. We also conjecture that our nano-crossbar design will be an effective approach for synthesizing high-performance customized arithmetic and logic circuits.
Show less - Date Issued
- 2014
- Identifier
- CFH0004571, ucf:45163
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFH0004571
- Title
- Predicting Students' Academic Performance with Decision Tree and Neural Network.
- Creator
-
Feng, Junshuai, Jha, Sumit Kumar, Zhang, Wei, Zhang, Shaojie, University of Central Florida
- Abstract / Description
-
Educational Data Mining (EDM) is a developing research field that involves many techniques to explore data relating to educational background. EDM can analyze and resolve educational data with computational methods to address educational questions. Similar to EDM, neural networks have been utilized in widespread and successful data mining applications. In this paper, synthetic datasets are employed since this paper aims to explore the methodologies such as decision tree classifiers and neural...
Show moreEducational Data Mining (EDM) is a developing research field that involves many techniques to explore data relating to educational background. EDM can analyze and resolve educational data with computational methods to address educational questions. Similar to EDM, neural networks have been utilized in widespread and successful data mining applications. In this paper, synthetic datasets are employed since this paper aims to explore the methodologies such as decision tree classifiers and neural networks to predict student performance in the context of EDM. Firstly, it introduces EDM and some relative works that have been accomplished previously in this field along with their datasets and computational results. Then, it demonstrates how the synthetic student dataset is generated, analyzes some input attributes from the dataset such as gender and high school GPA, and delivers with some visualization results to determine which classification methods approaches are the most efficient. After testing the data with decision tree classifiers and neural networks methodologies, it concludes the effectiveness of both approaches in terms of the model evaluation performance as well as discussing some of the most promising future work of this research.
Show less - Date Issued
- 2019
- Identifier
- CFE0007455, ucf:52680
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007455
- Title
- Approximate Binary Decision Diagrams for High-Performance Computing.
- Creator
-
Sivakumar, Anagha, Jha, Sumit Kumar, Leavens, Gary, Valliyil Thankachan, Sharma, University of Central Florida
- Abstract / Description
-
Many soft applications such as machine learning and probabilistic computational modeling can benefit from approximate but high-performance implementations. In this thesis, we study how Binary decision diagrams (BDDs) can be used to synthesize approximate high-performance implementations from high-level specifications such as program kernels written in a C-like language. We demonstrate the potential of our approach by designing nanoscale crossbars from such approximate Boolean decision...
Show moreMany soft applications such as machine learning and probabilistic computational modeling can benefit from approximate but high-performance implementations. In this thesis, we study how Binary decision diagrams (BDDs) can be used to synthesize approximate high-performance implementations from high-level specifications such as program kernels written in a C-like language. We demonstrate the potential of our approach by designing nanoscale crossbars from such approximate Boolean decision diagrams. Our work may be useful in designing massively-parallel approximate crossbar computing systems for application-specific domains such as probabilistic computational modeling.
Show less - Date Issued
- 2018
- Identifier
- CFE0007414, ucf:52704
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007414
- Title
- Categorical range reporting in 2D using Wavelet tree.
- Creator
-
Kanthareddy Sumithra, Swathi, Valliyil Thankachan, Sharma, Sundaram, Kalpathy, Jha, Sumit Kumar, University of Central Florida
- Abstract / Description
-
The research involved optimizing the space and bounding the output time by the output size in categorical range reporting of points within the given rectangle query Q in two dimension using wavelet trees and range counting. The time taken to report those points and space to tore n points in set S can be done using wavelet tree and range counting. Consider set S consisting of n points in two-dimension. An orthogonal range reporting query rectangle Q = [a,b] x [c,d] on set S is sent to report...
Show moreThe research involved optimizing the space and bounding the output time by the output size in categorical range reporting of points within the given rectangle query Q in two dimension using wavelet trees and range counting. The time taken to report those points and space to tore n points in set S can be done using wavelet tree and range counting. Consider set S consisting of n points in two-dimension. An orthogonal range reporting query rectangle Q = [a,b] x [c,d] on set S is sent to report the set of points in S which interacts with the query rectangle[Q]. The time taken to report these points is dependent on the output size. The categorical range reporting is an extension of orthogonal range reporting, where each point (xi; yi) in S is associated with a category c[i] belongs to [sigma] and the query is to report the set of distinct categories within the query region [a,b] x [c,d] once. In this paper, we present a new solution for this problem using wavelet trees. The points in S associated with categories are stored in a wavelet tree structure. Wavelet tree structure consists of bit map for these categories. To report the categories in the given rectangle queryQ, rank and select operations on the wavelet tree is applied. It was observed that the space taken by the structure was O(n log sigma) space and query time is O(k log n log sigma). Notice that the new result is more efficient in space when log sigma = O(log n). The study provides a new and efficient way of storing large dataset and also bounds the time complexity by the output size k.
Show less - Date Issued
- 2018
- Identifier
- CFE0007204, ucf:52275
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007204
- Title
- Student Community Detection and Recommendation of Customized Paths to Reinforce Academic Success.
- Creator
-
Shao, Yuan, Jha, Sumit Kumar, Zhang, Wei, Zhang, Shaojie, University of Central Florida
- Abstract / Description
-
Educational Data Mining (EDM) is a research area that analyzes educational data and extracts interesting and unique information to address education issues. EDM implements computational methods to explore data for the purpose of studying questions related to educational achievements. A common task in an educational environment is the grouping of students and the identification of communities that have common features. Then, these communities of students may be studied by a course developer to...
Show moreEducational Data Mining (EDM) is a research area that analyzes educational data and extracts interesting and unique information to address education issues. EDM implements computational methods to explore data for the purpose of studying questions related to educational achievements. A common task in an educational environment is the grouping of students and the identification of communities that have common features. Then, these communities of students may be studied by a course developer to build a personalized learning system, promote effective group learning, provide adaptive contents, etc. The objective of this thesis is to find an approach to detect student communities and analyze students who do well academically with particular sequences of classes in each community. Then, we compute one or more sequences of courses that a student in a community may pursue to higher their chances of obtaining good academic performance.
Show less - Date Issued
- 2019
- Identifier
- CFE0007529, ucf:52623
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007529
- Title
- Verification and Automated Synthesis of Memristor Crossbars.
- Creator
-
Pourtabatabaie, Arya, Jha, Sumit Kumar, Chatterjee, Mainak, Pattanaik, Sumanta, University of Central Florida
- Abstract / Description
-
The Memristor is a newly synthesized circuit element correlating differences in electrical charge and magnetic flux, which effectively acts as a nonlinear resistor with memory. The small size of this element and its potential for passive state preservation has opened great opportunities for data-level parallel computation, since the functions of memory and processing can be realized on the same physical device.In this research we present an in-depth study of memristor crossbars for...
Show moreThe Memristor is a newly synthesized circuit element correlating differences in electrical charge and magnetic flux, which effectively acts as a nonlinear resistor with memory. The small size of this element and its potential for passive state preservation has opened great opportunities for data-level parallel computation, since the functions of memory and processing can be realized on the same physical device.In this research we present an in-depth study of memristor crossbars for combinational and sequential logic. We outline the structure of formulas which they are able to produce and henceforth the inherent powers and limitations of Memristive Crossbar Computing.As an improvement on previous methods of automated crossbar synthesis, a method for symbolically verifying crossbars is proposed, proven and analysed.
Show less - Date Issued
- 2016
- Identifier
- CFE0006840, ucf:51765
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006840
- Title
- Adversarial Attacks On Vision Algorithms Using Deep Learning Features.
- Creator
-
Michel, Andy, Jha, Sumit Kumar, Leavens, Gary, Valliyil Thankachan, Sharma, University of Central Florida
- Abstract / Description
-
Computer vision algorithms, such as those implementing object detection, are known to be sus-ceptible to adversarial attacks. Small barely perceptible perturbations to the input can cause visionalgorithms to incorrectly classify inputs that they would have otherwise classified correctly. Anumber of approaches have been recently investigated to generate such adversarial examples fordeep neural networks. Many of these approaches either require grey-box access to the deep neuralnet being...
Show moreComputer vision algorithms, such as those implementing object detection, are known to be sus-ceptible to adversarial attacks. Small barely perceptible perturbations to the input can cause visionalgorithms to incorrectly classify inputs that they would have otherwise classified correctly. Anumber of approaches have been recently investigated to generate such adversarial examples fordeep neural networks. Many of these approaches either require grey-box access to the deep neuralnet being attacked or rely on adversarial transfer and grey-box access to a surrogate neural network.In this thesis, we present an approach to the synthesis of adversarial examples for computer vi-sion algorithms that only requires black-box access to the algorithm being attacked. Our attackapproach employs fuzzing with features derived from the layers of a convolutional neural networktrained on adversarial examples from an unrelated dataset. Based on our experimental results,we believe that our validation approach will enable designers of cyber-physical systems and otherhigh-assurance use-cases of vision algorithms to stress test their implementations.
Show less - Date Issued
- 2017
- Identifier
- CFE0006898, ucf:51714
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006898
- Title
- Learning robotic manipulation from user demonstrations.
- Creator
-
Rahmatizadeh, Rouhollah, Boloni, Ladislau, Turgut, Damla, Jha, Sumit Kumar, University of Central Florida
- Abstract / Description
-
Personal robots that help disabled or elderly people in their activities of daily living need to be able to autonomously perform complex manipulation tasks. Traditional approaches to this problem employ task-specific controllers. However, these must to be designed by expert programmers, are focused on a single task, and will perform the task as programmed, not according to the preferences of the user. In this dissertation, we investigate methods that enable an assistive robot to learn to...
Show morePersonal robots that help disabled or elderly people in their activities of daily living need to be able to autonomously perform complex manipulation tasks. Traditional approaches to this problem employ task-specific controllers. However, these must to be designed by expert programmers, are focused on a single task, and will perform the task as programmed, not according to the preferences of the user. In this dissertation, we investigate methods that enable an assistive robot to learn to execute tasks as demonstrated by the user. First, we describe a learning from demonstration (LfD) method that learns assistive tasks that need to be adapted to the position and orientation of the user's head. Then we discuss a recurrent neural network controller that learns to generate movement trajectories for the end-effector of the robot arm to accomplish a task. The input to this controller is the pose of related objects and the current pose of the end-effector itself. Next, we discuss how to extract user preferences from the demonstration using reinforcement learning. Finally, we extend this controller to one that learns to observe images of the environment and generate joint movements for the robot to accomplish a desired task. We discuss several techniques that improve the performance of the controller and reduce the number of required demonstrations. One of this is multi-task learning: learning multiple tasks simultaneously with the same neural network. Another technique is to make the controller output one joint at a time-step, therefore to condition the prediction of each joint on the previous joints. We evaluate these controllers on a set of manipulation tasks and show that they can learn complex tasks, overcome failure, and attempt a task several times until they succeed.
Show less - Date Issued
- 2017
- Identifier
- CFE0006908, ucf:51686
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006908
- Title
- Design of a JMLdoclet for JMLdoc in OpenJML.
- Creator
-
Donthala, Arjun Mitra Reddy, Leavens, Gary, Turgut, Damla, Jha, Sumit Kumar, University of Central Florida
- Abstract / Description
-
The Java Modeling Language (JML) is a behavioral interface specification language designed for specifying Java classes and interfaces. OpenJML is a tool for processing JML specifications of Java programs. To facilitate viewing of these specifications in a user-friendly manner, a tool JMLdoc was created. The JMLdoc tool adds JML specifications to the usual Javadoc documentation. JMLdoc is an enhancement of Javadoc that adds to the Javadoc documentation the JML specifications that are present...
Show moreThe Java Modeling Language (JML) is a behavioral interface specification language designed for specifying Java classes and interfaces. OpenJML is a tool for processing JML specifications of Java programs. To facilitate viewing of these specifications in a user-friendly manner, a tool JMLdoc was created. The JMLdoc tool adds JML specifications to the usual Javadoc documentation. JMLdoc is an enhancement of Javadoc that adds to the Javadoc documentation the JML specifications that are present in the source code. The JMLdoc tool is a drop-in replacement for Javadoc, with additional functionality and additional options. The current design of JMLdoc uses the standard Javadoc's doclet. The current design lacks the provision for doclet extensions, unlike Javadoc. This thesis proposes a new design which is more aligned with the design of Javadoc and its provision for doclet extensions by implementing a JMLdoclet: a new doclet for OpenJML with support for JML elements. The new design makes JMLdoc independent of Javadoc's internals. This way maintenance is reduced as Javadoc evolves. The new design also combines specifications from inheritance and refinements and presents the complete JML specification to the user. This new doclet based design will be more maintainable and easier to extend.
Show less - Date Issued
- 2016
- Identifier
- CFE0006295, ucf:51596
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006295
- Title
- Finding Consensus Energy Folding Landscapes Between RNA Sequences.
- Creator
-
Burbridge, Joshua, Zhang, Shaojie, Hu, Haiyan, Jha, Sumit, University of Central Florida
- Abstract / Description
-
In molecular biology, the secondary structure of a ribonucleic acid (RNA) molecule is closely related to its biological function. One problem in structural bioinformatics is to determine the two- and three-dimensional structure of RNA using only sequencing information, which can be obtained at low cost. This entails designing sophisticated algorithms to simulate the process of RNA folding using detailed sets of thermodynamic parameters. The set of all chemically feasible structures an RNA...
Show moreIn molecular biology, the secondary structure of a ribonucleic acid (RNA) molecule is closely related to its biological function. One problem in structural bioinformatics is to determine the two- and three-dimensional structure of RNA using only sequencing information, which can be obtained at low cost. This entails designing sophisticated algorithms to simulate the process of RNA folding using detailed sets of thermodynamic parameters. The set of all chemically feasible structures an RNA molecule can assume, as well as the energy associated with each structure, is called its energy folding landscape. This research focuses on defining and solving the problem of finding the consensus landscape between multiple RNA molecules. Specifically, we discuss how this problem is equivalent to the problem of Balanced Global Network Alignment, and what effect a solution to this problem would have on our understanding of RNA.Because this problem is known to be NP-hard, we instead define an approximate consensus on a landscape of reduced size, which dramatically reduces the searching space associated with the problem. We use the program RNASLOpt to enumerate all stable local optimal secondary structures in multiple landscapes within a certain energy and stability range of the minimum free energy (MFE) structure. We then encode these using an extended structural alphabet and perform sequence alignment using a structural substitution matrix to find and rank the best matches between the sets based on stability, energy, and structural distance. We apply this method to twenty landscapes from four sets of riboswitches from Bacillus subtillis in order to predict their native (")on(") and (")off(") structures. We find that this method significantly reduces the size of the list of candidate structures, as well as increasing the ranking of previously obscure secondary structures, resulting in more accurate predictions overall. Advances in the field of structural bioinformatics can help elucidate the underlying mechanisms of many genetic diseases.
Show less - Date Issued
- 2015
- Identifier
- CFE0006210, ucf:51109
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006210
- Title
- Implementation of Refining Statements in OpenJML and Verification of Higher Order Methods with Model Program Specifications.
- Creator
-
Gurramkonda, Sai Chandesh, Leavens, Gary, Turgut, Damla, Jha, Sumit Kumar, University of Central Florida
- Abstract / Description
-
The Java Modeling Language (JML) describes the functional behavior of Java classes and methods using pre- and postconditions. However, standard pre- and postcondition specifications cannot verify calls to higher order methods (HOMs). JML uses model program specifications to reason about HOMs. This thesis describes the implementation of model programs in the OpenJML tool. The implementation includes parsing, type checking, and matching of model program specifications against the code.
- Date Issued
- 2017
- Identifier
- CFE0006743, ucf:51831
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0006743
- Title
- Energy efficient routing towards a mobile sink using virtual coordinates in a wireless sensor network.
- Creator
-
Rahmatizadeh, Rouhollah, Boloni, Ladislau, Turgut, Damla, Jha, Sumit, University of Central Florida
- Abstract / Description
-
The existence of a coordinate system can often improve the routing in a wireless sensor network. While most coordinate systems correspond to the geometrical or geographical coordinates, in recent years researchers had proposed the use of virtual coordinates. Virtual coordinates depend only on the topology of the network as defined by the connectivity of the nodes, without requiring geographical information. The work in this thesis extends the use of virtual coordinates to scenarios where the...
Show moreThe existence of a coordinate system can often improve the routing in a wireless sensor network. While most coordinate systems correspond to the geometrical or geographical coordinates, in recent years researchers had proposed the use of virtual coordinates. Virtual coordinates depend only on the topology of the network as defined by the connectivity of the nodes, without requiring geographical information. The work in this thesis extends the use of virtual coordinates to scenarios where the wireless sensor network has a mobile sink. One reason to use a mobile sink is to distribute the energy consumption more evenly among the sensor nodes and thus extend the life-time of the network. We developed two algorithms, MS-DVCR and CU-DVCR which perform routing towards a mobile sink using virtual coordinates. In contrast to the baseline virtual coordinate routing MS-DVCR limits routing updates triggered by the sink movement to a local area around the sink. In contrast, CU-DVCR limits the route updates to a circular area on the boundary of the local area. We describe the design justification and the implementation of these algorithms. Using a set of experimental studies, we show that MS-DVCR and CU-DVCR achieve a lower energy consumption compared to the baseline virtual coordinate routing without any noticeable impact on routing performance. In addition, CU-DVCR provides a lower energy consumption than MS-DVCR for the case of a fast moving sink.
Show less - Date Issued
- 2014
- Identifier
- CFE0005402, ucf:50422
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0005402
- Title
- Reasoning Tradeoffs in Implicit Invocation and Aspect Oriented Languages.
- Creator
-
Sanchez Salazar, Jose, Leavens, Gary, Turgut, Damla, Jha, Sumit, Martin, Heath, University of Central Florida
- Abstract / Description
-
To reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming...
Show moreTo reason about a program means to state or conclude, by logical means, some properties the program exhibits; like its correctness according to certain expected behavior. The continuous need for more ambitious, more complex, and more dependable software systems demands for better mechanisms to modularize them and reason about their correctness. The reasoning process is affected by the design decisions made by the developer of the program and by the features supported by the programming language used. Beyond Object Orientation, Implicit Invocation and Aspect Oriented languages pose very hard reasoning challenges. Important tradeoffs must be considered while reasoning about a program: modular vs. non-modular reasoning, case-by-case analysis vs. abstraction, explicitness vs. implicitness; are some of them. By deciding a series of tradeoffs one can configure a reasoning scenario. For example if one decides for modular reasoning and explicit invocation a well-known object oriented reasoning scenario can be used.This dissertation identifies various important tradeoffs faced when reasoning about implicit invocation and aspect oriented programs, characterize scenarios derived from making choices regarding these tradeoffs, and provides sound proof rules for verification of programs covered by all these scenarios. Guidance for program developers and language designers is also given, so that reasoning about these types of programs becomes more tractable.
Show less - Date Issued
- 2015
- Identifier
- CFE0005706, ucf:50133
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0005706
- Title
- A deep learning approach to diagnosing schizophrenia.
- Creator
-
Barry, Justin, Valliyil Thankachan, Sharma, Gurupur, Varadraj, Jha, Sumit Kumar, Ewetz, Rickard, University of Central Florida
- Abstract / Description
-
In this article, the investigators present a new method using a deep learning approach to diagnose schizophrenia. In the experiment presented, the investigators have used a secondary dataset provided by National Institutes of Health. The aforementioned experimentation involves analyzing this dataset for existence of schizophrenia using traditional machine learning approaches such as logistic regression, support vector machine, and random forest. This is followed by application of deep...
Show moreIn this article, the investigators present a new method using a deep learning approach to diagnose schizophrenia. In the experiment presented, the investigators have used a secondary dataset provided by National Institutes of Health. The aforementioned experimentation involves analyzing this dataset for existence of schizophrenia using traditional machine learning approaches such as logistic regression, support vector machine, and random forest. This is followed by application of deep learning techniques using three hidden layers in the model. The results obtained indicate that deep learning provides state-of-the-art accuracy in diagnosing schizophrenia. Based on these observations, there is a possibility that deep learning may provide a paradigm shift in diagnosing schizophrenia.
Show less - Date Issued
- 2019
- Identifier
- CFE0007429, ucf:52737
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007429
- Title
- In-Memory Computing Using Formal Methods and Paths-Based Logic.
- Creator
-
Velasquez, Alvaro, Jha, Sumit Kumar, Leavens, Gary, Wu, Annie, Subramani, K., University of Central Florida
- Abstract / Description
-
The continued scaling of the CMOS device has been largely responsible for the increase in computational power and consequent technological progress over the last few decades. However, the end of Dennard scaling has interrupted this era of sustained exponential growth in computing performance. Indeed, we are quickly reaching an impasse in the form of limitations in the lithographic processes used to fabricate CMOS processes and, even more dire, we are beginning to face fundamental physical...
Show moreThe continued scaling of the CMOS device has been largely responsible for the increase in computational power and consequent technological progress over the last few decades. However, the end of Dennard scaling has interrupted this era of sustained exponential growth in computing performance. Indeed, we are quickly reaching an impasse in the form of limitations in the lithographic processes used to fabricate CMOS processes and, even more dire, we are beginning to face fundamental physical phenomena, such as quantum tunneling, that are pervasive at the nanometer scale. Such phenomena manifests itself in prohibitively high leakage currents and process variations, leading to inaccurate computations. As a result, there has been a surge of interest in computing architectures that can replace the traditional CMOS transistor-based methods. This thesis is a thorough investigation of how computations can be performed on one such architecture, called a crossbar. The methods proposed in this document apply to any crossbar consisting of two-terminal connective devices. First, we demonstrate how paths of electric current between two wires can be used as design primitives in a crossbar. We then leverage principles from the field of formal methods, in particular the area of bounded model checking, to automate the synthesis of crossbar designs for computing arithmetic operations. We demonstrate that our approach yields circuits that are state-of-the-art in terms of the number of operations required to perform a computation. Finally, we look at the benefits of using a 3D crossbar for computation; that is, a crossbar consisting of multiple layers of interconnects. A novel 3D crossbar computing paradigm is proposed for solving the Boolean matrix multiplication and transitive closure problems and we show how this paradigm can be utilized, with small modifications, in the XPoint crossbar memory architecture that was recently announced by Intel.
Show less - Date Issued
- 2018
- Identifier
- CFE0007419, ucf:52720
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007419
- Title
- Soft-Error Resilience Framework For Reliable and Energy-Efficient CMOS Logic and Spintronic Memory Architectures.
- Creator
-
Alghareb, Faris, DeMara, Ronald, Lin, Mingjie, Zou, Changchun, Jha, Sumit Kumar, Song, Zixia, University of Central Florida
- Abstract / Description
-
The revolution in chip manufacturing processes spanning five decades has proliferated high performance and energy-efficient nano-electronic devices across all aspects of daily life. In recent years, CMOS technology scaling has realized billions of transistors within large-scale VLSI chips to elevate performance. However, these advancements have also continually augmented the impact of Single-Event Transient (SET) and Single-Event Upset (SEU) occurrences which precipitate a range of Soft-Error...
Show moreThe revolution in chip manufacturing processes spanning five decades has proliferated high performance and energy-efficient nano-electronic devices across all aspects of daily life. In recent years, CMOS technology scaling has realized billions of transistors within large-scale VLSI chips to elevate performance. However, these advancements have also continually augmented the impact of Single-Event Transient (SET) and Single-Event Upset (SEU) occurrences which precipitate a range of Soft-Error (SE) dependability issues. Consequently, soft-error mitigation techniques have become essential to improve systems' reliability. Herein, first, we proposed optimized soft-error resilience designs to improve robustness of sub-micron computing systems. The proposed approaches were developed to deliver energy-efficiency and tolerate double/multiple errors simultaneously while incurring acceptable speed performance degradation compared to the prior work. Secondly, the impact of Process Variation (PV) at the Near-Threshold Voltage (NTV) region on redundancy-based SE-mitigation approaches for High-Performance Computing (HPC) systems was investigated to highlight the approach that can realize favorable attributes, such as reduced critical datapath delay variation and low speed degradation. Finally, recently, spin-based devices have been widely used to design Non-Volatile (NV) elements such as NV latches and flip-flops, which can be leveraged in normally-off computing architectures for Internet-of-Things (IoT) and energy-harvesting-powered applications. Thus, in the last portion of this dissertation, we design and evaluate for soft-error resilience NV-latching circuits that can achieve intriguing features, such as low energy consumption, high computing performance, and superior soft errors tolerance, i.e., concurrently able to tolerate Multiple Node Upset (MNU), to potentially become a mainstream solution for the aerospace and avionic nanoelectronics. Together, these objectives cooperate to increase energy-efficiency and soft errors mitigation resiliency of larger-scale emerging NV latching circuits within iso-energy constraints. In summary, addressing these reliability concerns is paramount to successful deployment of future reliable and energy-efficient CMOS logic and spintronic memory architectures with deeply-scaled devices operating at low-voltages.
Show less - Date Issued
- 2019
- Identifier
- CFE0007884, ucf:52765
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007884
- Title
- Advancing Practical Specification Techniques for Modern Software Systems.
- Creator
-
Singleton, John, Leavens, Gary, Jha, Sumit Kumar, Zou, Changchun, Hughes, Charles, Brennan, Joseph, University of Central Florida
- Abstract / Description
-
The pervasive nature of software (and the tendency for it to contain errors) has long been a concern of theoretical computer scientists. Many investigators have endeavored to produce theories, tools, and techniques for verifying the behavior of software systems. One of the most promising lines of research is that of formal specification, which is a subset of the larger field of formal methods. In formal specification, one composes a precise mathematical description of a software system and...
Show moreThe pervasive nature of software (and the tendency for it to contain errors) has long been a concern of theoretical computer scientists. Many investigators have endeavored to produce theories, tools, and techniques for verifying the behavior of software systems. One of the most promising lines of research is that of formal specification, which is a subset of the larger field of formal methods. In formal specification, one composes a precise mathematical description of a software system and uses tools and techniques to ensure that the software that has been written conforms to this specification. Examples of such systems are Z notation, the Java Modeling Language, and many others. However, a fundamental problem that plagues this line of research is that the specifications themselves are often costly to produce and difficult to reuse. If the field of formal specification is to advance, we must develop sound techniques for reducing the cost of producing and reusing software specifications. The work presented in this dissertation lays out a path to producing sophisticated, automated tools for inferring large, complex code bases, tools for allowing engineers to share and reuse specifications, and specification languages for specifying information flow policies that can be written separately from program code. This dissertation introduces three main lines of research. First, I discuss a system that facilitates the authoring, sharing, and reuse of software specifications. Next, I discuss a technique which aims to reduce the cost of producing specifications by automatically inferring them. Finally, I discuss a specification language called Evidently which aims to make information flow security policies easier to write, maintain, and enforce by untangling them from the code to which they are applied.
Show less - Date Issued
- 2018
- Identifier
- CFE0007099, ucf:51953
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007099
- Title
- reasoning about frame properties in object-oriented programs.
- Creator
-
Bao, Yuyan, Leavens, Gary, Dechev, Damian, Jha, Sumit Kumar, Cash, Mason, University of Central Florida
- Abstract / Description
-
Framing is important for specification and verification of object-oriented programs.This dissertation develops the local reasoning approach for framing in the presence of data structures with unrestricted sharing and subtyping.It can verify shared data structures specified in a concise way by unifying fine-grained region logic and separation logic. Then the fine-grained region logic is extended to reason about subtyping.First, fine-grained region logic is adapted from region logic to express...
Show moreFraming is important for specification and verification of object-oriented programs.This dissertation develops the local reasoning approach for framing in the presence of data structures with unrestricted sharing and subtyping.It can verify shared data structures specified in a concise way by unifying fine-grained region logic and separation logic. Then the fine-grained region logic is extended to reason about subtyping.First, fine-grained region logic is adapted from region logic to express regions at the granularity of individual fields. Conditional region expressions are introduced; not only does this allow one to specify more precise frame conditions, it also has the ability to express footprints of separation logic assertions.Second, fine-grained region logic is generalized to a new logic called unified fine-grained region logic by allowing the logic to restrict the heap in which a program runs. This feature allows one to express specifications in separation logic.Third, both fine-grained region logic and separation logic can be encoded to unified fine-grained region logic. This result allows the proof system to reason about programs specified in both styles.Finally, fine-grained region logic is extended to reason about a programming language that is similar to Java. To reason about inheritance locally, a frame condition for behavioral subtyping is defined and proved sound.
Show less - Date Issued
- 2017
- Identifier
- CFE0007279, ucf:52195
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007279
- Title
- Automated Synthesis of Unconventional Computing Systems.
- Creator
-
Hassen, Amad Ul, Jha, Sumit Kumar, Sundaram, Kalpathy, Fan, Deliang, Ewetz, Rickard, Rahman, Talat, University of Central Florida
- Abstract / Description
-
Despite decades of advancements, modern computing systems which are based on the von Neumann architecture still carry its shortcomings. Moore's law, which had substantially masked the effects of the inherent memory-processor bottleneck of the von Neumann architecture, has slowed down due to transistor dimensions nearing atomic sizes. On the other hand, modern computational requirements, driven by machine learning, pattern recognition, artificial intelligence, data mining, and IoT, are growing...
Show moreDespite decades of advancements, modern computing systems which are based on the von Neumann architecture still carry its shortcomings. Moore's law, which had substantially masked the effects of the inherent memory-processor bottleneck of the von Neumann architecture, has slowed down due to transistor dimensions nearing atomic sizes. On the other hand, modern computational requirements, driven by machine learning, pattern recognition, artificial intelligence, data mining, and IoT, are growing at the fastest pace ever. By their inherent nature, these applications are particularly affected by communication-bottlenecks, because processing them requires a large number of simple operations involving data retrieval and storage. The need to address the problems associated with conventional computing systems at the fundamental level has given rise to several unconventional computing paradigms. In this dissertation, we have made advancements for automated syntheses of two types of unconventional computing paradigms: in-memory computing and stochastic computing. In-memory computing circumvents the problem of limited communication bandwidth by unifying processing and storage at the same physical locations. The advent of nanoelectronic devices in the last decade has made in-memory computing an energy-, area-, and cost-effective alternative to conventional computing. We have used Binary Decision Diagrams (BDDs) for in-memory computing on memristor crossbars. Specifically, we have used Free-BDDs, a special class of binary decision diagrams, for synthesizing crossbars for flow-based in-memory computing. Stochastic computing is a re-emerging discipline with several times smaller area/power requirements as compared to conventional computing systems. It is especially suited for fault-tolerant applications like image processing, artificial intelligence, pattern recognition, etc. We have proposed a decision procedures-based iterative algorithm to synthesize Linear Finite State Machines (LFSM) for stochastically computing non-linear functions such as polynomials, exponentials, and hyperbolic functions.
Show less - Date Issued
- 2019
- Identifier
- CFE0007648, ucf:52462
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007648
- Title
- Machine Learning Methods for Multiparameter Flow Cytometry Analysis and Visualization.
- Creator
-
Sassano, Emily, Jha, Sumit Kumar, Pattanaik, Sumanta, Hughes, Charles, Moore, Sean, University of Central Florida
- Abstract / Description
-
Flow cytometry is a popular analytical cell-biology instrument that uses specific wavelengths of light to profile heterogeneous populations of cells at the individual level. Current cytometers have the capability of analyzing up to 20 parameters on over a million cells, but despite the complexity of these datasets, a typical workflow relies on subjective labor-intensive manual sequential analysis. The research presented in this dissertation provides two machine learning methods to increase...
Show moreFlow cytometry is a popular analytical cell-biology instrument that uses specific wavelengths of light to profile heterogeneous populations of cells at the individual level. Current cytometers have the capability of analyzing up to 20 parameters on over a million cells, but despite the complexity of these datasets, a typical workflow relies on subjective labor-intensive manual sequential analysis. The research presented in this dissertation provides two machine learning methods to increase the objectivity, efficiency, and discovery in flow cytometry data analysis. The first, a supervised learning method, utilizes previously analyzed data to evaluate new flow cytometry files containing similar parameters. The probability distribution of each dimension in a file is matched to each related dimension of a reference file through color indexing and histogram intersection methods. Once a similar reference file is selected the cell populations previously classified are used to create a tailored support vector machine capable of classifying cell populations as an expert would. This method has produced results highly correlated with manual sequential analysis, providing an efficient alternative for analyzing a large number of samples. The second, a novel unsupervised method, is used to explore and visualize single-cell data in an objective manner. To accomplish this, a hypergraph sampling method was created to preserve rare events within the flow data before divisively clustering the sampled data using singular value decomposition. The unsampled data is added to the discovered set of clusters using a support vector machine classifier, and the final analysis is displayed as a minimum spanning tree. This tree is capable of distinguishing rare subsets of cells comprising of less than 1% of the original data.
Show less - Date Issued
- 2018
- Identifier
- CFE0007243, ucf:52241
- Format
- Document (PDF)
- PURL
- http://purl.flvc.org/ucf/fd/CFE0007243
