Doctor of Philosophy, The Ohio State University, 2021, Computer Science and Engineering

Modular verification of parallel and concurrent software built from reusable data abstractions is a challenging problem. Reasoning about sequential software can be modularized using the specifications of data abstractions, but the need to consider implementation details complicates reasoning about parallel execution. Addressing this challenge requires advancing the state of the art in several ways, beginning with a theoretical foundation. The A/P Calculus for describing the effects of program actions is developed in this dissertation to enable sound modular reasoning about parallel programs with non-interfering parallel sections of operation calls on abstract data types. Building on the calculus and a programming language with clean semantics, a methodology for designing decomposable data abstractions is presented to produce fork-join parallel programs that are manifestly data race free and readily amenable to modular reasoning. A new specification construct, the non-interference contract, is proposed to enhance the specification of data abstractions to hide implementation details and yet facilitate modular reasoning about parallel programs that share objects among processes. As a key first step to transition these results to practice, this dissertation describes Clean++, a discipline for writing software in C++ that leverages move semantics to make ownership transfer the primary data movement operation (as opposed to either deep or shallow copying) and produce programs that are amenable to formal verification with only minimal scaffolding related to pointer manipulation.

Committee: Paolo A.G. Sivilotti (Advisor); Murali Sitaraman (Committee Member); Neelam Soundarajan (Committee Member); Michael Bond (Committee Member) Subjects: Computer Science

MS, University of Cincinnati, 2004, Engineering : Industrial Engineering

A major shortcoming of the current solid modeling schemes is their inability to store tolerance information. Lack of tolerance information makes it almost impossible to integrate computer-aided inspection with other modules of computer integrated manufacturing systems. If geometric tolerance information can be incorporated in CAD data structures, it will play a key role in the overall integration that the modern manufacturing industry is starving for. The current work is an attempt to make further inroads in this relatively new arena. A comprehensive tolerance information capturing system is proposed in this project. This system stores tolerance zone information in parametric form. It is mathematical, compact and compatible with current solid model data structures. An automated inspection system is developed that uses this stored information to verify actual feature conformance with the specified tolerance. Variational geometric models and space data transformations are central to this system. New concepts such as datum adjusted nominal feature and sequential tolerance verification algorithm are introduced. The system also has one component that checks for inconsistencies in tolerance specifications in the design stage. Overall, the system can perform many tasks in the inspection process for which currently human expert is required.

Committee: Dr. Sam Anand (Advisor) Subjects: Engineering, Industrial

Doctor of Philosophy, The Ohio State University, 2011, Computer Science and Engineering

In order to have more confidence in software-based systems, we would like to be able to show automatically that a particular software component meets its specification; the component does what it is supposed to do. Testing can increase confidence in software; however, testing alone cannot show that software meets its specification, only that no errors have been found yet. We are building stronger tools for increasing our confidence in software in response to the verifying compiler grand challenge. The vision is that all software will include specifications for all of the operations of a component (including pre- and post-conditions) along with code annotations in a purported implementation (including loop invariants, and progress metrics for the termination of both loops and recursive operations). These annotations allow us to generate verification conditions (VCs) that represent the correctness of the code mathematically. The code meets its specification and is correct if the VCs are proved. We focus on the problem of automating VC proofs and examining potential obstacles for automated proofs. More specifically, this dissertation defends the following three-part thesis: 1. Modest changes in programming languages may effectively support and facilitate automated verification without introducing an undue annotation burden on programmers. 2. An interactive proof assistant can be an effective back-end prover for automated software verification. 3. Translations between similar formal systems present significant challenges in fully automating software verification.

Committee: Bruce W. Weide PhD (Advisor); Paul A. G. Sivilotti PhD (Committee Member); Michael D. Bond PhD (Other) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2011, Computer Science and Engineering

For a variety of reasons, software must evolve to cope with change. Unfortunately, evolution and maintenance is an expensive, time-consuming, and error-prone task, especially when the system in question is large and complex. Typically, a change to a single program element requires changes to related, and often seemingly unrelated, elements scattered throughout the source code. To address this problem, approaches have emerged to mechanically assist developers with a wide range of software evolution and maintenance tasks. This assistance is typically provided in the form of extensions (plug-ins) to integrated development environments (IDEs) that afford (semi-) automated aid in carrying out these tasks, thus easing the burden associated with evolution and maintenance. Although existing approaches are useful in alleviating some of the burden associated with software evolution and maintenance, there are a number of situations where developers are still required to complete evolution and maintenance tasks manually. Automated approaches to assist developers with such cumbersome and error-prone tasks would be extremely useful in evolving and maintaining large, complex systems. In this thesis, I develop several new techniques that can be of great value to software developers in evolving code to accommodate change. The first is an automated refactoring that upgrades legacy Java code to use proper language enumeration (enum) types, a feature of the modern Java language. I have developed an approach that preserves semantics and that allows us to migrate legacy applications by automatically replacing a predominantly used pattern with suitable use of enums. The second technique is an automated approach to assist developers in maintaining pointcuts in evolving Aspect-Oriented (AO) programs. AO languages enable developers to better encapsulate crosscutting concern (CCC) implementations by allowing them to create an expression (a pointcut) which specifies well-defined points ( (open full item for complete abstract)

Committee: Neelam Soundarajan PhD (Advisor); Atanas Rountev PhD (Committee Member); Paul A. G. Sivilotti PhD (Committee Member); Paul Evans PhD (Committee Member) Subjects: Computer Science

Doctor of Philosophy, The Ohio State University, 2010, Computer Science and Engineering

Numerous pieces of the software verification puzzle need to fit together in order to achieve that vision. First, there must be a programming language that gives some hope of specifying and implementing verifiable code ("assertive code"). Second, there needs to be a correct procedure for generating verification conditions (VCs) from this assertive code. Third, there must be one or more automated theorem provers to process the VCs and determine their validity or invalidity. Finally, it is essential that there is an interface for programmers to write their code and verify or debug it without forcing them to understand how particular automated theorem provers work. This dissertation covers the latter two of these topics using the Resolve language and verification framework. A common failing of most automated verification techniques is the inability to be truly automatic in all circumstances. Experience with proof assistants shows that they need to be "nudged" in the correct direction by an intervening human, in all but the simplest cases. Otherwise, the option is to use tools not geared to handle the rich mathematics used in the Resolve programming language. By using specialized decision procedures that take into account the known structure of the generated VCs, we strive to accomplish one of two possibilities for each VC: first, we hope to prove it outright; otherwise, we hope to simplify the VC to such an extent that another prover is able to handle it. We detail work on SplitDecision, a tool that simplifies VCs for Resolve. We further explain work that has helped to ensure SplitDecision is among the fastest and least memory intensive automated provers available, by introducing "lazy copying" to Resolve/C++ (in which SplitDecision is written), with specific work to maintain the value semantics integral to Resolve's design. Sometimes (perhaps this is even the modal case) at least one VC is not proved because it is not valid. It is clear that the ways we present errors (open full item for complete abstract)

Committee: Bruce Weide PhD (Advisor); Atanas Rountev PhD (Committee Member); Paolo Sivilotti PhD (Committee Member); Melvin Pascall PhD (Committee Member) Subjects: Computer Science