View All Items

Title: Data Mining Models for Tackling High Dimensional Datasets and Outliers.
Creator: Panagopoulos, Orestis, Xanthopoulos, Petros, Rabelo, Luis, Zheng, Qipeng, Dechev, Damian, University of Central Florida
Abstract / Description: High dimensional data and the presence of outliers in data each pose a serious challenge in supervised learning.Datasets with significantly larger number of features compared to samples arise in various areas, including business analytics and biomedical applications. Such datasets pose a serious challenge to standard statistical methods and render many existing classification techniques impractical. The generalization ability of many classification algorithms is compromised due to the so...
Show moreHigh dimensional data and the presence of outliers in data each pose a serious challenge in supervised learning.Datasets with significantly larger number of features compared to samples arise in various areas, including business analytics and biomedical applications. Such datasets pose a serious challenge to standard statistical methods and render many existing classification techniques impractical. The generalization ability of many classification algorithms is compromised due to the so-called curse of dimensionality. A new binary classification method called constrained subspace classifier (CSC) is proposed for such high dimensional datasets. CSC improves on an earlier proposed classification method called local subspace classifier (LSC) by accounting for the relative angle between subspaces while approximating the classes with individual subspaces. CSC is formulated as an optimization problem and can be solved by an efficient alternating optimization technique. Classification performance is tested in publicly available datasets. The improvement in classification accuracy over LSC shows the importance of considering the relative angle between the subspaces while approximating the classes. Additionally, CSC appears to be a robust classifier, compared to traditional two step methods that perform feature selection and classification in two distinct steps.Outliers can be present in real world datasets due to noise or measurement errors. The presence of outliers can affect the training phase of machine learning algorithms, leading to over-fitting which results in poor generalization ability. A new regression method called relaxed support vector regression (RSVR) is proposed for such datasets. RSVR is based on the concept of constraint relaxation which leads to increased robustness in datasets with outliers. RSVR is formulated using both linear and quadratic loss functions. Numerical experiments on benchmark datasets and computational comparisons with other popular regression methods depict the behavior of our proposed method. RSVR achieves better overall performance than support vector regression (SVR) in measures such as RMSE and $R^2_{adj}$ while being on par with other state-of-the-art regression methods such as robust regression (RR). Additionally, RSVR provides robustness for higher dimensional datasets which is a limitation of RR, the robust equivalent of ordinary least squares regression. Moreover, RSVR can be used on datasets that contain varying levels of noise.Lastly, we present a new novelty detection model called relaxed one-class support vector machines (ROSVMs) that deals with the problem of one-class classification in the presence of outliers.
Show less
Date Issued: 2016
Identifier: CFE0006698, ucf:51920
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006698

Title: Correctness and Progress Verification of Non-Blocking Programs.
Creator: Peterson, Christina, Dechev, Damian, Leavens, Gary, Bassiouni, Mostafa, Cash, Mason, University of Central Florida
Abstract / Description: The progression of multi-core processors has inspired the development of concurrency libraries that guarantee safety and liveness properties of multiprocessor applications. The difficulty of reasoning about safety and liveness properties in a concurrent environment has led to the development of tools to verify that a concurrent data structure meets a correctness condition or progress guarantee. However, these tools possess shortcomings regarding the ability to verify a composition of data...
Show moreThe progression of multi-core processors has inspired the development of concurrency libraries that guarantee safety and liveness properties of multiprocessor applications. The difficulty of reasoning about safety and liveness properties in a concurrent environment has led to the development of tools to verify that a concurrent data structure meets a correctness condition or progress guarantee. However, these tools possess shortcomings regarding the ability to verify a composition of data structure operations. Additionally, verification techniques for transactional memory evaluate correctness based on low-level read/write histories, which is not applicable to transactional data structures that use a high-level semantic conflict detection.In my dissertation, I present tools for checking the correctness of multiprocessor programs that overcome the limitations of previous correctness verification techniques. Correctness Condition Specification (CCSpec) is the first tool that automatically checks the correctness of a composition of concurrent multi-container operations performed in a non-atomic manner. Transactional Correctness tool for Abstract Data Types (TxC-ADT) is the first tool that can check the correctness of transactional data structures. TxC-ADT elevates the standard definitions of transactional correctness to be in terms of an abstract data type, an essential aspect for checking correctness of transactions that synchronize only for high-level semantic conflicts. Many practical concurrent data structures, transactional data structures, and algorithms to facilitate non-blocking programming all incorporate helping schemes to ensure that an operation comprising multiple atomic steps is completed according to the progress guarantee. The helping scheme introduces additional interference by the active threads in the system to achieve the designed progress guarantee. Previous progress verification techniques do not accommodate loops whose termination is dependent on complex behaviors of the interfering threads, making these approaches unsuitable. My dissertation presents the first progress verification technique for non-blocking algorithms that are dependent on descriptor-based helping mechanisms.
Show less
Date Issued: 2019
Identifier: CFE0007705, ucf:52433
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0007705

Title: Practical Dynamic Transactional Data Structures.
Creator: Laborde, Pierre, Dechev, Damian, Leavens, Gary, Turgut, Damla, Mucciolo, Eduardo, University of Central Florida
Abstract / Description: Multicore programming presents the challenge of synchronizing multiple threads.Traditionally, mutual exclusion locks are used to limit access to a shared resource to a single thread at a time.Whether this lock is applied to an entire data structure, or only a single element, the pitfalls of lock-based programming persist.Deadlock, livelock, starvation, and priority inversion are some of the hazards of lock-based programming that can be avoided by using non-blocking techniques.Non-blocking...
Show moreMulticore programming presents the challenge of synchronizing multiple threads.Traditionally, mutual exclusion locks are used to limit access to a shared resource to a single thread at a time.Whether this lock is applied to an entire data structure, or only a single element, the pitfalls of lock-based programming persist.Deadlock, livelock, starvation, and priority inversion are some of the hazards of lock-based programming that can be avoided by using non-blocking techniques.Non-blocking data structures allow scalable and thread-safe access to shared data by guaranteeing, at least, system-wide progress.In this work, we present the first wait-free hash map which allows a large number of threads to concurrently insert, get, and remove information.Wait-freedom means that all threads make progress in a finite amount of time --- an attribute that can be critical in real-time environments.We only use atomic operations that are provided by the hardware; therefore, our hash map can be utilized by a variety of data-intensive applications including those within the domains of embedded systems and supercomputers.The challenges of providing this guarantee make the design and implementation of wait-free objects difficult.As such, there are few wait-free data structures described in the literature; in particular, there are no wait-free hash maps.It often becomes necessary to sacrifice performance in order to achieve wait-freedom.However, our experimental evaluation shows that our hash map design is, on average, 7 times faster than a traditional blocking design.Our solution outperforms the best available alternative non-blocking designs in a large majority of cases, typically by a factor of 15 or higher.The main drawback of non-blocking data structures is that only one linearizable operation can be executed by each thread, at any one time.To overcome this limitation we present a framework for developing dynamic transactional data containers.Transactional containers are those that execute a sequence of operations atomically and in such a way that concurrent transactions appear to take effect in some sequential order.We take an existing algorithm that transforms non-blocking sets into static transactional versions (LFTT), and we modify it to support maps.We implement a non-blocking transactional hash map using this new approach.We continue to build on LFTT by implementing a lock-free vector using a methodology to allow LFTT to be compatible with non-linked data structures.A static transaction requires all operands and operations to be specified at compile-time, and no code may be executed between transactions.These limitations render static transactions impractical for most use cases.We modify LFTT to support dynamic transactions, and we enhance it with additional features.Dynamic transactions allow operands to be specified at runtime rather than compile-time, and threads can execute code between the data structure operations of a transaction.We build a framework for transforming non-blocking containers into dynamic transactional data structures, called Dynamic Transactional Transformation (DTT), and provide a library of novel transactional containers.Our library provides the wait-free progress guarantee and supports transactions among multiple data structures, whereas previous work on data structure transactions has been limited to operating on a single container.Our approach is 3 times faster than software transactional memory, and its performance matches its lock-free transactional counterpart.
Show less
Date Issued: 2018
Identifier: CFE0007215, ucf:52212
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0007215

Title: JML Template Generation.
Creator: Poojari, Kushal Raghav, Leavens, Gary, Turgut, Damla, Dechev, Damian, University of Central Florida
Abstract / Description: The Java Modeling Language (JML) is a behavioral interface specific language designed to specify Java modules (which are Java classes and interfaces). Specifications are used to describe the intended functionality without considering the way it is implemented. In JML, if a user wants to write specifications for a Java file, he or she must undertake several steps. To help automate the process of creating annotations for method specifications, a tool Jmlspec was created. Jmlspec generated a...
Show moreThe Java Modeling Language (JML) is a behavioral interface specific language designed to specify Java modules (which are Java classes and interfaces). Specifications are used to describe the intended functionality without considering the way it is implemented. In JML, if a user wants to write specifications for a Java file, he or she must undertake several steps. To help automate the process of creating annotations for method specifications, a tool Jmlspec was created. Jmlspec generated a file that refines the source file and has empty placeholders in which one can write specifications. Although Jmlspec worked with older versions of Java, it does not work with the current version of Java (Java 8). This thesis describes the implementation of a new version of the Jmlspec tool that is compatible with newest versions of Java. This tool will be more maintainable than the older version of Jmlspec and easier to extend.
Show less
Date Issued: 2017
Identifier: CFE0006641, ucf:51228
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006641

Title: The Design, Implementation, and Refinement of Wait-Free Algorithms and Containers.
Creator: Feldman, Steven, Dechev, Damian, Heinrich, Mark, Orooji, Ali, Mucciolo, Eduardo, University of Central Florida
Abstract / Description: My research has been on the development of concurrent algorithms for shared memory systems that provide guarantees of progress.Research into such algorithms is important to developers implementing applications on mission critical and time sensitive systems.These guarantees of progress provide safety properties and freedom from many hazards, such as dead-lock, live-lock, and thread starvation.In addition to the safety concerns, the fine-grained synchronization used in implementing these...
Show moreMy research has been on the development of concurrent algorithms for shared memory systems that provide guarantees of progress.Research into such algorithms is important to developers implementing applications on mission critical and time sensitive systems.These guarantees of progress provide safety properties and freedom from many hazards, such as dead-lock, live-lock, and thread starvation.In addition to the safety concerns, the fine-grained synchronization used in implementing these algorithms promises to provide scalable performance in massively parallel systems.My research has resulted in the development of wait-free versions of the stack, hash map, ring buffer, vector, and a multi-word compare-and-swap algorithms.Through this experience, I have learned and developed new techniques and methodologies for implementing non-blocking and wait-free algorithms.I have worked with and refined existing techniques to improve their practicality and applicability.In the creation of the aforementioned algorithms, I have developed an association model for use with descriptor-based operations.This model, originally developed for the multi-word compare-and-swap algorithm, has been applied to the design of the vector and ring buffer algorithms.To unify these algorithms and techniques, I have released Tervel, a wait-free library of common algorithms and containers.This library includes a framework that simplifies and improves the design of non-blocking algorithms.I have reimplemented several algorithms using this framework and the resulting implementation exhibits less code duplication and fewer perceivable states.When reimplementing algorithms, I have adapted their Application Programming Interface (API) specification to remove ambiguity and non-deterministic behavior found when using a sequential API in a concurrent environment.To improve the performance of my algorithm implementations, I extended OVIS's Lightweight Distributed Metric Service (LDMS)'s data collection and transport system to support performance monitoring using perf_event and PAPI libraries.These libraries have provided me with deeper insights into the behavior of my algorithms, and I was able to use these insights to improve the design and performance of my algorithms.
Show less
Date Issued: 2015
Identifier: CFE0005946, ucf:50813
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0005946

Title: High-Performance Composable Transactional Data Structures.
Creator: Zhang, Deli, Dechev, Damian, Leavens, Gary, Zou, Changchun, Lin, Mingjie, University of Central Florida
Abstract / Description: Exploiting the parallelism in multiprocessor systems is a major challenge in the post ``power wall'' era. Programming for multicore demands a change in the way we design and use fundamental data structures. Concurrent data structures allow scalable and thread-safe accesses to shared data. They provide operations that appear to take effect atomically when invoked individually.A main obstacle to the practical use of concurrent data structures is their inability to support composable operations,...
Show moreExploiting the parallelism in multiprocessor systems is a major challenge in the post ``power wall'' era. Programming for multicore demands a change in the way we design and use fundamental data structures. Concurrent data structures allow scalable and thread-safe accesses to shared data. They provide operations that appear to take effect atomically when invoked individually.A main obstacle to the practical use of concurrent data structures is their inability to support composable operations, i.e., to execute multiple operations atomically in a transactional manner. The problem stems from the inability of concurrent data structure to ensure atomicity of transactions composed from operations on a single or multiple data structures instances. This greatly hinders software reuse because users can only invoke data structure operations in a limited number of ways.Existing solutions, such as software transactional memory (STM) and transactional boosting, manage transaction synchronization in an external layer separated from the data structure's own thread-level concurrency control. Although this reduces programming effort, it leads to significant overhead associated with additional synchronization and the need to rollback aborted transactions. In this dissertation, I address the practicality and efficiency concerns by designing, implementing, and evaluating high-performance transactional data structures that facilitate the development of future highly concurrent software systems.Firstly, I present two methodologies for implementing high-performance transactional data structures based on existing concurrent data structures using either lock-based or lock-free synchronizations. For lock-based data structures, the idea is to treat data accessed by multiple operations as resources. The challenge is for each thread to acquire exclusive access to desired resources while preventing deadlock or starvation. Existing locking strategies, like two-phase locking and resource hierarchy, suffer from performance degradation under heavy contention, while lacking a desirable fairness guarantee. To overcome these issues, I introduce a scalable lock algorithm for shared-memory multiprocessors addressing the resource allocation problem. It is the first multi-resource lock algorithm that guarantees the strongest first-in, first-out (FIFO) fairness. For lock-free data structures, I present a methodology for transforming them into high-performance lock-free transactional data structures without revamping the data structures' original synchronization design. My approach leverages the semantic knowledge of the data structure to eliminate the overhead of false conflicts and rollbacks.Secondly, I apply the proposed methodologies and present a suite of novel transactional search data structures in the form of an open source library. This is interesting not only because the fundamental importance of search data structures in computer science and their wide use in real world programs, but also because it demonstrate the implementation issues that arise when using the methodologies I have developed. This library is not only a compilation of a large number of fundamental data structures for multiprocessor applications, but also a framework for enabling composable transactions, and moreover, an infrastructure for continuous integration of new data structures. By taking such a top-down approach, I am able to identify and consider the interplay of data structure interface operations as a whole, which allows for scrutinizing their commutativity rules and hence opens up possibilities for design optimizations.Lastly, I evaluate the throughput of the proposed data structures using transactions with randomly generated operations on two difference hardware systems. To ensure the strongest possible competition, I chose the best performing alternatives from state-of-the-art locking protocols and transactional memory systems in the literature. The results show that it is straightforward to build efficient transactional data structures when using my multi-resource lock as a drop-in replacement for transactional boosted data structures. Furthermore, this work shows that it is possible to build efficient lock-free transactional data structures with all perceived benefits of lock-freedom and with performance far better than generic transactional memory systems.
Show less
Date Issued: 2016
Identifier: CFE0006428, ucf:51453
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006428

Title: TryOpenJML - A Verily based web application for learning about the Java Modeling Language.
Creator: Deshpande, Tushar, Leavens, Gary, Turgut, Damla, Dechev, Damian, University of Central Florida
Abstract / Description: This thesis has a two-fold purpose. On the one hand, the web applications are an important part of life. On a day to day basis, from managing our heath care choices to banking, to connecting to a friend, almost everything is done through a web application. Development of these applications is also a very trend-driven domain. Numerous web frameworks are available today, but almost none has been created taking reliability into consideration. With the combination of application construction...
Show moreThis thesis has a two-fold purpose. On the one hand, the web applications are an important part of life. On a day to day basis, from managing our heath care choices to banking, to connecting to a friend, almost everything is done through a web application. Development of these applications is also a very trend-driven domain. Numerous web frameworks are available today, but almost none has been created taking reliability into consideration. With the combination of application construction recipes and static analysis, the Verily framework was created to build more reliable web applications.On the other hand, the goal of the Java Modeling Language (JML) has to be conveyed to the world. It is a language that can go hand in hand with existing code, having a wide range of tools that help build practical and effective designs. There are many tools available for JML: jmldoc for web pages, jmlunit for unit tests, jmlc for class files, etc. I will be using the tools for Runtime Assertion Checking (RAC) and Extended Static Checking (ESC). These checks warn about the possible runtime exceptions and assertion violations. The benefits of JML assert statements over Java assertions are that they support all JML features.The question that I am concerned with, in this thesis, is how the Verily Framework can contribute to the domain of web application development. Keeping this question in mind, my objective is to create a tutorial which will aid in learning about JML. The tutorial will let the potential users read and write JML specifications and use JML tools, explain basic JML semantics, and let them know where to go for help if they need more details.
Show less
Date Issued: 2016
Identifier: CFE0006293, ucf:51614
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006293

Title: Analysis of Commutativity with state-chart graph representation of concurrent programs.
Creator: Debnath, Kishore, Dechev, Damian, Leavens, Gary, Bassiouni, Mostafa, University of Central Florida
Abstract / Description: We present a new approach to check for Commutativity in concurrent programs from their run-time state-chart graphs. Two operations are said to be commutative if changing the order of their execution do not change the resultant effect on the working object. Commutative property is capable of boosting performance in concurrent transactions such that transactional concurrency is comparable to a non-blocking linearizable version of a similar data structure type. Transactional concurrency is a...
Show moreWe present a new approach to check for Commutativity in concurrent programs from their run-time state-chart graphs. Two operations are said to be commutative if changing the order of their execution do not change the resultant effect on the working object. Commutative property is capable of boosting performance in concurrent transactions such that transactional concurrency is comparable to a non-blocking linearizable version of a similar data structure type. Transactional concurrency is a technique that analyses object semantics, as object states, to determine conflicts and recovery between conflicting operations. Processes that commute at object level can be executed concurrently at transaction level without conflicting with one another. In our approach we generate graphs by tracking run-time execution of concurrent program and representing object states in all possible thread interleavings as states and transitions. Using state-chart notations, we capture the object states at each execution step and compare their states before and after transitions as processed by a known set of operations reordered in different ways. Considering the non-deterministic nature of concurrent programs, we exhaustively capture program states during method invocation, method response, atomic instruction execution, etc., for determining commutativity. This helps user to examine state transitions at a thread level granularity, across all possible interleavings. With this methodology user can not only verify commutativity, but also can visually check ways in which functions commute at object level, which is an edge over current state-of-the art tools. The object level commutative information helps in identifying faulty implementations and performance improving considerations. We use a graph database to represent state nodes that further assists to check for other concurrency properties using cypher queries.
Show less
Date Issued: 2016
Identifier: CFE0006290, ucf:51608
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006290

Title: A Comparison of Concurrent Correctness Criteria for Shared Memory Based Data Structure.
Creator: Bhattacharya, Dipanjan, Dechev, Damian, Leavens, Gary, Bassiouni, Mostafa, University of Central Florida
Abstract / Description: Developing concurrent algorithms requires safety and liveness to be defined in order to understand their proper behavior. Safety refers to the correctness criteria while liveness is the progress guarantee. Nowadays there are a variety of correctness conditions for concurrent objects. The way these correctness conditions differ and the various trade-offs they present with respect to performance, usability, and progress guarantees is poorly understood. This presents a daunting task for the...
Show moreDeveloping concurrent algorithms requires safety and liveness to be defined in order to understand their proper behavior. Safety refers to the correctness criteria while liveness is the progress guarantee. Nowadays there are a variety of correctness conditions for concurrent objects. The way these correctness conditions differ and the various trade-offs they present with respect to performance, usability, and progress guarantees is poorly understood. This presents a daunting task for the developers and users of such concurrent algorithms who are trying to better understand the correctness of their code and the various trade-offs associated with their design choices and use. The purpose of this study is to explore the set of known correctness conditions for concurrent objects, find their correlations and categorize them, and provide insights regarding their implications with respect to performance and usability. In this thesis, a comparative study of Linearizability, Sequential Consistency, Quiescent Consistency and Quasi Linearizability will be presented using data structures like FIFO Queues, Stacks, and Priority Queues, and with a case study for performance of these implementations using different correctness criteria.
Show less
Date Issued: 2016
Identifier: CFE0006263, ucf:51046
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006263

Title: A Compiler-based Framework for Automatic Extraction of Program Skeletons for Exascale Hardware/Software Co-design.
Creator: Rudraiah Dakshinamurthy, Amruth, Dechev, Damian, Heinrich, Mark, Deo, Narsingh, University of Central Florida
Abstract / Description: The design of high-performance computing architectures requires performance analysis of large-scale parallel applications to derive various parameters concerning hardware design and software development. The process of performance analysis and benchmarking an application can be done in several ways with varying degrees of fidelity. One of the most cost-effective ways is to do a coarse-grained study of large-scale parallel applications through the use of program skeletons. The concept of a `...
Show moreThe design of high-performance computing architectures requires performance analysis of large-scale parallel applications to derive various parameters concerning hardware design and software development. The process of performance analysis and benchmarking an application can be done in several ways with varying degrees of fidelity. One of the most cost-effective ways is to do a coarse-grained study of large-scale parallel applications through the use of program skeletons. The concept of a ``program skeleton'' that we discuss in this paper is an abstracted program that is derived from a larger program where source code that is determined to be irrelevant is removed for the purposes of the skeleton. In this work, we develop a semi-automatic approach for extracting program skeletons based on compiler program analysis. We demonstrate correctness of our skeleton extraction process by comparing details from communication traces, as well as show the performance speedup of using skeletons by running simulations in the SST/macro simulator. Extracting such a program skeleton from a large-scale parallel program requires a substantial amount of manual effort and often introduces human errors. We outline a semi-automatic approach for extracting program skeletons from large-scale parallel applications that reduces cost and eliminates errors inherent in manual approaches. Our skeleton generation approach is based on the use of the extensible and open-source ROSE compiler infrastructure that allows us to perform flow and dependency analysis on larger programs in order to determine what code can be removed from the program to generate a skeleton.
Show less
Date Issued: 2013
Identifier: CFE0004743, ucf:49795
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0004743

Title: Using Freebase, an Automatically Generated Dictionary, and a Classifier to Identify a Person's Profession in Tweets.
Creator: Hall, Abraham, Gomez, Fernando, Dechev, Damian, Tappen, Marshall, University of Central Florida
Abstract / Description: Algorithms for classifying pre-tagged person entities in tweets into one of eight profession categories are presented. A classifier using a semi-supervised learning algorithm that takes into consideration the local context surrounding the entity in the tweet, hash tag information, and topic signature scores is described. In addition to the classifier, this research investigates two dictionaries containing the professions of persons. These two dictionaries are used in their own classification...
Show moreAlgorithms for classifying pre-tagged person entities in tweets into one of eight profession categories are presented. A classifier using a semi-supervised learning algorithm that takes into consideration the local context surrounding the entity in the tweet, hash tag information, and topic signature scores is described. In addition to the classifier, this research investigates two dictionaries containing the professions of persons. These two dictionaries are used in their own classification algorithms which are independent of the classifier. The method for creating the first dictionary dynamically from the web and the algorithm that accesses this dictionary to classify a person into one of the eight profession categories are explained next. The second dictionary is freebase, an openly available online database that is maintained by its online community. The algorithm that uses freebase for classifying a person into one of the eight professions is described. The results also show that classifications made using the automated constructed dictionary, freebase, or the classifier are all moderately successful. The results also show that classifications made with the automated constructed person dictionary are slightly more accurate than classifications made using freebase. Various hybrid methods, combining the classifier and the two dictionaries are also explained. The results of those hybrid methods show significant improvement over any of the individual methods.
Show less
Date Issued: 2013
Identifier: CFE0004858, ucf:49715
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0004858

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: The Power of Quantum Walk: Insights, Implementation, and Applications.
Creator: Chiang, Chen-Fu, Wocjan, Pawel, Marinescu, Dan, Dechev, Damian, Mucciolo, Eduardo, University of Central Florida
Abstract / Description: In this thesis, I investigate quantum walks in quantum computing from threeaspects: the insights, the implementation, and the applications. Quantum walks are the quantum analogue of classical random walks. For the insights of quantum walks, I list and explain the required components for quantizing a classical random walk into a quantum walk. The components are, for instance, Markov chains, quantum phase estimation, and quantum spectrum theorem. I then demonstrate how the product of two...
Show moreIn this thesis, I investigate quantum walks in quantum computing from threeaspects: the insights, the implementation, and the applications. Quantum walks are the quantum analogue of classical random walks. For the insights of quantum walks, I list and explain the required components for quantizing a classical random walk into a quantum walk. The components are, for instance, Markov chains, quantum phase estimation, and quantum spectrum theorem. I then demonstrate how the product of two reflections in the walk operator provides a quadratic speed-up, in comparison to the classical counterpart. For the implementation of quantum walks, I show the construction of an efficient circuit for realizing one single step of the quantum walk operator. Furthermore, I devise a more succinct circuit to approximately implement quantum phase estimation with constant precision controlled phase shift operators. From an implementation perspective, efficient circuits are always desirable because the realization of a phase shift operator with high precision would be a costly task and a critical obstacle. For the applications of quantum walks, I apply the quantum walk technique along with other fundamental quantum techniques, such as phase estimation, to solve the partition function problem. However, there might be some scenario in which the speed-up of spectral gap is insignificant. In a situation like that that,I provide an amplitude amplification-based approach to prepare the thermal Gibbs state. Such an approach is useful when the spectral gap is extremely small. Finally, I further investigate and explore the effect of noise (perturbation)on the performance of quantum walks.
Show less
Date Issued: 2011
Identifier: CFE0004094, ucf:49148
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0004094

Title: Data Representation in Machine Learning Methods with its Application to Compilation Optimization and Epitope Prediction.
Creator: Sher, Yevgeniy, Zhang, Shaojie, Dechev, Damian, Leavens, Gary, Gonzalez, Avelino, Zhi, Degui, University of Central Florida
Abstract / Description: In this dissertation we explore the application of machine learning algorithms to compilation phase order optimization, and epitope prediction. The common thread running through these two disparate domains is the type of data being dealt with. In both problem domains we are dealing with categorical data, with its representation playing a significant role in the performance of classification algorithms.We first present a neuroevolutionary approach which orders optimization phases to generate...
Show moreIn this dissertation we explore the application of machine learning algorithms to compilation phase order optimization, and epitope prediction. The common thread running through these two disparate domains is the type of data being dealt with. In both problem domains we are dealing with categorical data, with its representation playing a significant role in the performance of classification algorithms.We first present a neuroevolutionary approach which orders optimization phases to generate compiled programs with performance superior to those compiled using LLVM's -O3 optimization level. Performance improvements calculated as the speed of the compiled program's execution ranged from 27% for the ccbench program, to 40.8% for bzip2.This dissertation then explores the problem of data representation of 3D biological data, such as amino acids. A new approach for distributed representation of 3D biological data through the process of embedding is proposed and explored. Analogously to word embedding, we developed a system that uses atomic and residue coordinates to generate distributed representation for residues, which we call 3D Residue BioVectors. Preliminary results are presented which demonstrate that even the low dimensional 3D Residue BioVectors can be used to predict conformational epitopes and protein-protein interactions, with promising proficiency. The generation of such 3D BioVectors, and the proposed methodology, opens the door for substantial future improvements, and application domains.The dissertation then explores the problem domain of linear B-Cell epitope prediction. This problem domain deals with predicting epitopes based strictly on the protein sequence. We present the DRREP system, which demonstrates how an ensemble of shallow neural networks can be combined with string kernels and analytical learning algorithm to produce state of the art epitope prediction results. DRREP was tested on the SARS subsequence, the HIV, Pellequer, AntiJen datasets, and the standard SEQ194 test dataset. AUC improvements achieved over the state of the art ranged from 3% to 8%.Finally, we present the SEEP epitope classifier, which is a multi-resolution SMV ensemble based classifier which uses conjoint triad feature representation, and produces state of the art classification results. SEEP leverages the domain specific knowledge based protein sequence encoding developed within the protein-protein interaction research domain. Using an ensemble of multi-resolution SVMs, and a sliding window based pre and post processing pipeline, SEEP achieves an AUC of 91.2 on the standard SEQ194 test dataset, a 24% improvement over the state of the art.
Show less
Date Issued: 2017
Identifier: CFE0006793, ucf:51829
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006793

formal verification (2)	+ -
lock-free (2)	+ -
non-blocking (2)	+ -
wait-free (2)	+ -
Analytics (1)	+ -

Classifier (1)	+ -
Commutativity (1)	+ -
Complexity of Design (1)	+ -
Concurrency (1)	+ -
Concurrent Data Structure (1)	+ -
Concurrent programs (1)	+ -
Correctness Criteria (1)	+ -
Data Mining (1)	+ -
Data Representation (1)	+ -
Data Structures (1)	+ -
Dependency Analysis (1)	+ -
Epitope Prediction (1)	+ -
Freebase (1)	+ -
Graph (1)	+ -
High Dimensional Data (1)	+ -
Hoare logic (1)	+ -
JML (1)	+ -
JML Template Generation (1)	+ -
Java Modeling Language (1)	+ -
Lock-free Programming (1)	+ -
Machine Learning (1)	+ -
Markov chain (1)	+ -
Named Entity Recognition (1)	+ -
OpenJML (1)	+ -
Optimization Phase Ordering Problem (1)	+ -

Dechev, Damian (14)	+ -
University of Central Florida (14)	+ -
Leavens, Gary (9)	+ -
Bassiouni, Mostafa (3)	+ -
Mucciolo, Eduardo (3)	+ -

Turgut, Damla (3)	+ -
Cash, Mason (2)	+ -
Heinrich, Mark (2)	+ -
Bao, Yuyan (1)	+ -
Bhattacharya, Dipanjan (1)	+ -
Chiang, Chen-Fu (1)	+ -
Debnath, Kishore (1)	+ -
Deo, Narsingh (1)	+ -
Deshpande, Tushar (1)	+ -
Feldman, Steven (1)	+ -
Gomez, Fernando (1)	+ -
Gonzalez, Avelino (1)	+ -
Hall, Abraham (1)	+ -
Jha, Sumit Kumar (1)	+ -
Laborde, Pierre (1)	+ -
Lin, Mingjie (1)	+ -
Marinescu, Dan (1)	+ -
Orooji, Ali (1)	+ -
Panagopoulos, Orestis (1)	+ -
Peterson, Christina (1)	+ -
Poojari, Kushal Raghav (1)	+ -
Rabelo, Luis (1)	+ -
Rudraiah Dakshinamurthy, Amruth (1)	+ -
Sher, Yevgeniy (1)	+ -
Tappen, Marshall (1)	+ -

Search In

Sort Results By:

Narrow results by:

Topical Subject

Collection

Type of Resource

Language

Creator

Format

Owner