Physical Sciences and Mathematics Commons^™

Deepcause: Verifying Neural Networks With Abstraction Refinement, Nguyen Hua Gia Phuc

Dissertations and Theses Collection (Open Access)

Neural networks have been becoming essential parts in many safety-critical systems (such
as self-driving cars and medical diagnosis). Due to that, it is desirable that neural networks
not only have high accuracy (which traditionally can be validated using a test set) but also
satisfy some safety properties (such as robustness, fairness, or free of backdoor). To verify
neural networks against desired safety properties, there are many approaches developed
based on classical abstract interpretation. However, like in program verification, these
approaches suffer from false alarms, which may hinder the deployment of the networks.

One natural remedy to tackle the problem adopted …

Formally Designing And Implementing Cyber Security Mechanisms In Industrial Control Networks., Mehdi Sabraoui

Electronic Theses and Dissertations

This dissertation describes progress in the state-of-the-art for developing and deploying formally verified cyber security devices in industrial control networks. It begins by detailing the unique struggles that are faced in industrial control networks and why concepts and technologies developed for securing traditional networks might not be appropriate. It uses these unique struggles and examples of contemporary cyber-attacks targeting control systems to argue that progress in securing control systems is best met with formal verification of systems, their specifications, and their security properties. This dissertation then presents a development process and identifies two technologies, TLA+ and seL4, that can be …

Shared-Environment Call-By-Need, George W. Stelle

Computer Science ETDs

Call-by-need semantics formalize the wisdom that work should be done at most once. It frees programmers to focus more on the correctness of their code, and less on the operational details. Because of this property, programmers of lazy functional languages rely heavily on their compiler to both preserve correctness and generate high-performance code for high level abstractions. In this dissertation I present a novel technique for compiling call-by-need semantics by using shared environments to share results of computation. I show how the approach enables a compiler that generates high-performance code, while staying simple enough to lend itself to formal reasoning. …

Logic -> Proof -> Rest, Maxwell Taylor

Senior Independent Study Theses

REST is a common architecture for networked applications. Applications that adhere to the REST constraints enjoy significant scaling advantages over other architectures. But REST is not a panacea for the task of building correct software. Algebraic models of computation, particularly CSP, prove useful to describe the composition of applications using REST. CSP enables us to describe and verify the behavior of RESTful systems. The descriptions of each component can be used independently to verify that a system behaves as expected. This thesis demonstrates and develops CSP methodology to verify the behavior of RESTful applications.

A Runtime Verification And Validation Framework For Self-Adaptive Software, David B. Sayre

CCE Theses and Dissertations

The concepts that make self-adaptive software attractive also make it more difficult for users to gain confidence that these systems will consistently meet their goals under uncertain context. To improve user confidence in self-adaptive behavior, machine-readable conceptual models have been developed to instrument the adaption behavior of the target software system and primary feedback loop. By comparing these machine-readable models to the self-adaptive system, runtime verification and validation may be introduced as another method to increase confidence in self-adaptive systems; however, the existing conceptual models do not provide the semantics needed to institute this runtime verification or validation. This research …

Verification Of Task Parallel Programs Using Predictive Analysis, Radha Vi Nakade

Theses and Dissertations

Task parallel programming languages provide a way for creating asynchronous tasks that can run concurrently. The advantage of using task parallelism is that the programmer can write code that is independent of the underlying hardware. The runtime determines the number of processor cores that are available and the most efficient way to execute the tasks. When two or more concurrently executing tasks access a shared memory location and if at least one of the accesses is for writing, data race is observed in the program. Data races can introduce non-determinism in the program output making it important to have data …

Design And Verification Environment For High-Performance Video-Based Embedded Systems, Michael Mefenza Nentedem

Graduate Theses and Dissertations

In this dissertation, a method and a tool to enable design and verification of computation demanding embedded vision-based systems is presented. Starting with an executable specification in OpenCV, we provide subsequent refinements and verification down to a system-on-chip prototype into an FPGA-Based smart camera. At each level of abstraction, properties of image processing applications are used along with structure composition to provide a generic architecture that can be automatically verified and mapped to the lower abstraction level. The result is a framework that encapsulates the computer vision library OpenCV at the highest level, integrates Accelera's System-C/TLM with UVM and QEMU-OS …

Design, Testing And Implementation Of A New Authentication Method Using Multiple Devices, Cagri Cetin

USF Tampa Graduate Theses and Dissertations

Authentication protocols are very common mechanisms to confirm the legitimacy of someone’s or something’s identity in digital and physical systems.

This thesis presents a new and robust authentication method based on users’ multiple devices. Due to the popularity of mobile devices, users are becoming more likely to have more than one device (e.g., smartwatch, smartphone, laptop, tablet, smart-car, smart-ring, etc.). The authentication system presented here takes advantage of these multiple devices to implement authentication mechanisms. In particular, the system requires the devices to collaborate with each other in order for the authentication to succeed. This new authentication protocol is robust …

Api Usage Verification Through Dataflow Analysis, Kenneth Baptiste Tapsoba

Theses and Dissertations

Using APIs in a program is often difficult because of the incomplete documentation and the shortage of available examples. To cope with that, we have seen the increase of API checking tools that provide efficient suggestions for API usage. However, most of those checking tools use a pattern-based analysis to determine errors such as misuse of API calls. In this thesis, we introduce a different analysis technique that relies on explicit API state transitions for the analysis of the program. We adopt a static dataflow analysis framework from SOOT to inspect state transitions at each program point.

Mining And Verification Of Temporal Events With Applications In Computer Micro-Architecture Research, Hui Meen Nyew

Dissertations, Master's Theses and Master's Reports - Open

Computer simulation programs are essential tools for scientists and engineers to understand a particular system of interest. As expected, the complexity of the software increases with the depth of the model used. In addition to the exigent demands of software engineering, verification of simulation programs is especially challenging because the models represented are complex and ridden with unknowns that will be discovered by developers in an iterative process. To manage such complexity, advanced verification techniques for continually matching the intended model to the implemented model are necessary. Therefore, the main goal of this research work is to design a useful …

Engineering Specifications And Mathematics For Verified Software, Hampton Smith

All Dissertations

Developing a verifying compiler---a compiler that proves that components are correct with respect to their specifications---is a grand challenge for the computing community. The prevailing view of the software engineering community is that this problem is necessarily difficult because, to-date, the resultant verification conditions necessary to prove software correctness have required powerful automated provers and deep mathematical insight to dispatch. This seems counter-intuitive, however, since human programmers only rarely resort to deep mathematics to assure themselves that their code works.
In this work, we show that well-specified and well-engineered software supported by a flexible, extensible mathematical system can yield verification …

Algorithms And Data Structures For Efficient Timing Analysis Of Asynchronous Real-Time Systems, Yingying Zhang

USF Tampa Graduate Theses and Dissertations

This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs).

In order to verify the real-time systems algorithmically, the zone-based timing analysis method is used for LPNs. It searches the state space with timing information (represented by zones). When there is a high degree of concurrency in the model, firing concurrent enabled transitions in different order may result in different zones, and these zones may be combined without affecting the verification result. Since the zone-based method could not deal with this problem efficiently, …

A Web-Integrated Environment For Component-Based Software Reasoning, Charles Cook

All Theses

This thesis presents the Web IDE, a web-integrated environment for component-based software reasoning. The Web IDE is specifically tailored to emphasize the relationships among various components in component-based software engineering (CBSE) and to facilitate reasoning. It allows students to use RESOLVE, a component-based, integrated specification and programming language, to build components and systems, providing real-time feedback that can be used to reason about the correctness of their component implementations. Real-time interaction and relationship focused component presentation reinforces CBSE and reasoning principles in a way not possible with traditional programming exercises and file management systems.
The Web IDE has gone through …

A Symbolic Approach Towards Constraint Based Software Verification, Shubhra Datta

Open Access Theses & Dissertations

Verification and validation (V&V) are two components of the software engineering process that are critical to achieve reliability that can account for up to 50% of the cost of software development. Numerous techniques ranging from formal proofs to testing methods exist to verify whether programs conform to their specifications. Recently, constraint programming techniques for V&V have emerged : they use the idea of proof by contradiction. They typically aim at proving that the code is inconsistent with the negation of the specification, which means that the software conforms to its specifications. Although the framework seems straightforward, the number of generated …

Using Live Sequence Chart Specifications For Formal Verification, Rahul Kumar

Theses and Dissertations

Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a …

Finding Termination And Time Improvement In Predicate Abstraction With Under-Approximation And Abstract Matching, Dritan Kudra

Theses and Dissertations

The focus of current formal verification methods is mitigating the state explosion problem. One of these formal methods is predicate abstraction, which reduces concrete states of a system to bitvectors of true/false valuations of a set of predicates. Predicate abstraction comes in two flavors, over-approximation and under-approximation. A drawback of over-approximation is that it produces too many spurious errors for data-intensive applications. A more recent under-approximation technique which does not produce spurious errors, does abstract matching on concrete states (AMCS). AMCS adds behaviors to an abstract system by augmenting the set of initial predicates, making use of a theorem prover. …

Dynamic Dead Variable Analysis, Micah S. Lewis

Theses and Dissertations

Dynamic dead variable analysis (DDVA) extends traditional static dead variable analysis (SDVA) in the context of model checking through the use of run-time information. The analysis is run multiple times during the course of model checking to create a more precise set of dead variables. The DDVA is evaluated based on the amount of memory used to complete model checking relative to SDVA while considering the extra overhead required to implement DDVA. On several models with a complex control flow graph, DDVA reduces the amount of memory needed by 38-88MB compared to SDVA with a cost of 36 bytes of …

Load Balancing Parallel Explicit State Model Checking, Rahul Kumar

Theses and Dissertations

This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory …