View All Items

Title: Examining Users' Application Permissions On Android Mobile Devices.
Creator: Safi, Muhammad, Wisniewski, Pamela, Leavens, Gary, Hughes, Charles, University of Central Florida
Abstract / Description: Mobile devices have become one of the most important computing platforms. The platform's portability and highly customized nature raises several privacy concerns. Therefore, understanding and predicting user privacy behavior has become very important if one is to design software which respects the privacy concerns of users. Various studies have been carried out to quantify user perceptions and concerns [23,36] and user characteristics which may predict privacy behavior [21,22,25]. Even though...
Show moreMobile devices have become one of the most important computing platforms. The platform's portability and highly customized nature raises several privacy concerns. Therefore, understanding and predicting user privacy behavior has become very important if one is to design software which respects the privacy concerns of users. Various studies have been carried out to quantify user perceptions and concerns [23,36] and user characteristics which may predict privacy behavior [21,22,25]. Even though significant research exists regarding factors which affect user privacy behavior, there is gap in the literature when it comes to correlating these factors to objectively collected data from user devices. We designed an Android application which administered surveys to collect various perceived measures, and to scrape past behavioral data from the phone. Our goal was to discover variables which help in predicting user location sharing decisions by correlating what we collected from surveys with the user's decision to share their location with our study application. We carried out logistic regression analysis with multiple measured variables and found that perceived measures and past behavioral data alone were poor predictors of user location sharing decisions. Instead, we discovered that perceived measures in the context of past behavior helped strengthen prediction models. Asking users to reflect on whether they were comfortable sharing their location with apps that were already installed on their mobile device was a stronger predictor of location sharing behavior than general measures regarding privacy concern or past behavioral data scraped from their phones. This work contributes to the field by correlating existing privacy measures with objective data, and uncovering a new predictor of location sharing decisions.
Show less
Date Issued: 2018
Identifier: CFE0007363, ucf:52085
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0007363

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: 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: Compiler Design of a Policy Specification Language for Conditional Gradual Release.
Creator: Kashyap Harinath, Manasa, Leavens, Gary, Turgut, Damla, Wang, Liqiang, University of Central Florida
Abstract / Description: Securing the confidentiality and integrity of information manipulated by computer software is an old yet increasingly important problem. Current software permission systems present on Android or iOS provide inadequate support for developing applications with secure information flow policies. To be useful, information flow control policies need to specify declassifications and the conditions under which declassification must occur. Having these declassifications scattered all over the program...
Show moreSecuring the confidentiality and integrity of information manipulated by computer software is an old yet increasingly important problem. Current software permission systems present on Android or iOS provide inadequate support for developing applications with secure information flow policies. To be useful, information flow control policies need to specify declassifications and the conditions under which declassification must occur. Having these declassifications scattered all over the program makes policies hard to find, which makes auditing difficult. To overcome these challenges, a policy specification language, 'Evidently' is discussed that allows one to specify information flow control policies separately from the program and which supports conditional gradual releases that can be automatically enforced. I discuss the Evidently grammar and modular semantics in detail. Finally, I discuss the implementational details of Evidently compiler within the Xtext language development environment and the implementation's enforcement of policies.
Show less
Date Issued: 2018
Identifier: CFE0007205, ucf:52274
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0007205

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: Specification and Runtime Checking of Timing Constraints in Safety Critical Java.
Creator: Haddad, Ghaith, Leavens, Gary, Turgut, Damla, Boloni, Ladislau, Nazzal, Dima, University of Central Florida
Abstract / Description: The Java platform is becoming a vital tool for developing real-time and safety-critical systems. Design patterns and the availability of Java libraries, both provide solutions to many known problems. Furthermore, the object-oriented nature of Java simplifies modular development of real-time systems. However, limitations of Java as a programming language for real-time systems are a notable obstacle to producing safe real-time systems. These limitations are found in the unpredictable execution...
Show moreThe Java platform is becoming a vital tool for developing real-time and safety-critical systems. Design patterns and the availability of Java libraries, both provide solutions to many known problems. Furthermore, the object-oriented nature of Java simplifies modular development of real-time systems. However, limitations of Java as a programming language for real-time systems are a notable obstacle to producing safe real-time systems. These limitations are found in the unpredictable execution model of the language, due to Java's garbage collector, and the lack of support for non-functional specification and verification tools. In this dissertation I introduce SafeJML, a specification language for support of functional and non-functional specifications, based on an implementation of a safety-critical Java platform and the Java Modeling Language (JML). This dissertation concentrates on techniques that enable specification and dynamic checking of timing constraints for some important Java features, including methods and subtyping. SafeJML and these dynamic checking techniques allow modular specification and checking of safety-critical systems, including those that use object-orientation and design patterns. Such coding techniques could have maintenance benefits for real-time and safety-critical software.
Show less
Date Issued: 2012
Identifier: CFE0004542, ucf:49224
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0004542

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: 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: DESIGNING LIGHT FILTERS TO DETECT SKIN USING A LOW-POWERED SENSOR.
Creator: Tariq, Muhammad, Wisniewski, Pamela, Gong, Boqing, Leavens, Gary, University of Central Florida
Abstract / Description: Detection of nudity in photos and videos, especially prior to uploading to the internet, is vital to solving many problems related to adolescent sexting, the distribution of child pornography, and cyber-bullying. The problem with using nudity detection algorithms as a means to combat these problems is that: 1) it implies that a digitized nude photo of a minor already exists (i.e., child pornography), and 2) there are real ethical and legal concerns around the distribution and processing of...
Show moreDetection of nudity in photos and videos, especially prior to uploading to the internet, is vital to solving many problems related to adolescent sexting, the distribution of child pornography, and cyber-bullying. The problem with using nudity detection algorithms as a means to combat these problems is that: 1) it implies that a digitized nude photo of a minor already exists (i.e., child pornography), and 2) there are real ethical and legal concerns around the distribution and processing of child pornography. Once a camera captures an image, that image is no longer secure. Therefore, we need to develop new privacy-preserving solutions that prevent the digital capture of nude imagery of minors. My research takes a first step in trying to accomplish this long-term goal: In this thesis, I examine the feasibility of using a low-powered sensor to detect skin dominance (defined as an image comprised of 50% or more of human skin tone) in a visual scene. By designing four custom light filters to enhance the digital information extracted from 300 scenes captured with the sensor (without digitizing high-fidelity visual features), I was able to accurately detect a skin dominant scene with 83.7% accuracy, 83% precision, and 85% recall. The long-term goal to be achieved in the future is to design a low-powered vision sensor that can be mounted on a digital camera lens on a teen's mobile device to detect and/or prevent the capture of nude imagery. Thus, I discuss the limitations of this work toward this larger goal, as well as future research directions.
Show less
Date Issued: 2017
Identifier: CFE0006806, ucf:51792
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006806

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: 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: 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: 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: Code Park: A New 3D Code Visualization Tool and IDE.
Creator: Khaloo, Pooya, Laviola II, Joseph, Foroosh, Hassan, Leavens, Gary, University of Central Florida
Abstract / Description: We introduce Code Park, a novel tool for visualizing codebases in a 3D game-like environment. Code Park aims to improve a programmer's understanding of an existing codebase in a manner that is both engaging and fun to be appealing especially for novice users such as students. It achieves these goals by laying out the codebase in a 3D park-like environment. Each class in the codebase is represented as a 3D room-like structure. Constituent parts of the class (variable, member functions, etc.)...
Show moreWe introduce Code Park, a novel tool for visualizing codebases in a 3D game-like environment. Code Park aims to improve a programmer's understanding of an existing codebase in a manner that is both engaging and fun to be appealing especially for novice users such as students. It achieves these goals by laying out the codebase in a 3D park-like environment. Each class in the codebase is represented as a 3D room-like structure. Constituent parts of the class (variable, member functions, etc.) are laid out on the walls, resembling a syntax-aware (")wallpaper("). The users can interact with the codebase using an overview, and a first-person viewer mode. They also can edit, compile and run code in this environment. We conducted three user studies to evaluate Code Park's usability and suitability for organizing an existing project. Our results indicate that Code Park is easy to get familiar with and significantly helps in code understanding. Further, the users unanimously believed that Code Park was an engaging tool to work with.
Show less
Date Issued: 2017
Identifier: CFE0006752, ucf:51838
Format: Document (PDF)
PURL: http://purl.flvc.org/ucf/fd/CFE0006752

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: 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: 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: 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

JML (5)	+ -
formal verification (3)	+ -
Evidently (2)	+ -
OpenJML (2)	+ -
approximate computing (2)	+ -

high-performance computing (2)	+ -
machine learning (2)	+ -
3d interaction (1)	+ -
Adversarial Attack (1)	+ -
Android (1)	+ -
Applications (1)	+ -
Artificial intelligence (1)	+ -
Aspect Orientation (1)	+ -
Automated synthesis (1)	+ -
Binary decision diagrams (1)	+ -
Checking (1)	+ -
Commutativity (1)	+ -
Complexity of Design (1)	+ -
Computer Vision (1)	+ -
Computer architecture (1)	+ -
Concurrency (1)	+ -
Concurrent Data Structure (1)	+ -
Concurrent programs (1)	+ -
Conditional Gradual Release (1)	+ -
Correctness Criteria (1)	+ -
Crossbar (1)	+ -
DNS (1)	+ -
Data Representation (1)	+ -
Data Structures (1)	+ -
Declassification (1)	+ -

Leavens, Gary (26)	+ -
University of Central Florida (26)	+ -
Dechev, Damian (9)	+ -
Turgut, Damla (9)	+ -
Jha, Sumit Kumar (8)	+ -

Bassiouni, Mostafa (4)	+ -
Hughes, Charles (3)	+ -
Valliyil Thankachan, Sharma (3)	+ -
Cash, Mason (2)	+ -
Jha, Sumit (2)	+ -
Wisniewski, Pamela (2)	+ -
Zou, Changchun (2)	+ -
Bagci, Ulas (1)	+ -
Bao, Yuyan (1)	+ -
Bhattacharya, Dipanjan (1)	+ -
Boloni, Ladislau (1)	+ -
Brennan, Joseph (1)	+ -
Chakraborty, Dwaipayan (1)	+ -
Debnath, Kishore (1)	+ -
Deshpande, Tushar (1)	+ -
Donthala, Arjun Mitra Reddy (1)	+ -
Elva, Rochelle (1)	+ -
Ewetz, Rickard (1)	+ -
Foroosh, Hassan (1)	+ -
Fu, Xinwen (1)	+ -
Gong, Boqing (1)	+ -
Gonzalez, Avelino (1)	+ -
Gurramkonda, Sai Chandesh (1)	+ -
Haddad, Ghaith (1)	+ -
Heinrich, Mark (1)	+ -

Search In

Pages

Pages

Sort Results By:

Narrow results by:

Topical Subject

Collection

Type of Resource

Language

Creator

Format

Owner