Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


thesis.pdf (769.23 KB)

ETD Abstract Container

Abstract Header

Contributions to Formal Specification and Modular Verification of Parallel and Sequential Software

Weide, Alan
http://orcid.org/0000-0003-1844-4630
http://rave.ohiolink.edu/etdc/view?acc_num=osu1638497327464541

Abstract Details

2021, Doctor of Philosophy, Ohio State University, 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.
Paolo A.G. Sivilotti (Advisor)
Murali Sitaraman (Committee Member)
Neelam Soundarajan (Committee Member)
Michael Bond (Committee Member)
223 p.
Computer Science
automated verification; automated reasoning; parallel programming; concurrent programming; C++; software engineering

Recommended Citations

Citations

  • Weide, A. (2021). Contributions to Formal Specification and Modular Verification of Parallel and Sequential Software [Doctoral dissertation, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu1638497327464541

    APA Style (7th edition)

  • Weide, Alan. Contributions to Formal Specification and Modular Verification of Parallel and Sequential Software. 2021. Ohio State University, Doctoral dissertation. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=osu1638497327464541.

    MLA Style (8th edition)

  • Weide, Alan. "Contributions to Formal Specification and Modular Verification of Parallel and Sequential Software." Doctoral dissertation, Ohio State University, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=osu1638497327464541

    Chicago Manual of Style (17th edition)

osu1638497327464541
129
© 2021, all rights reserved.
This open access ETD is published by The Ohio State University and OhioLINK.