Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


2021_MS_Rumreich.pdf (745.62 KB)

ETD Abstract Container

Abstract Header

The Binary Decision Diagram: Formal Verification of a Reference Implementation

Rumreich, Laine
http://rave.ohiolink.edu/etdc/view?acc_num=osu1618940583868248

Abstract Details

2021, Master of Science, Ohio State University, Computer Science and Engineering.
Formal verification is a method of proving program correctness based on formal specifications and using mathematics. The goal of this study is to formally verify by mathematical proof the correctness of a Java implementation of a Binary Decision Diagram (BDD). Specifically, the verification of the implementation proves its correctness and makes it significantly less susceptible to errors, crashing, and undiscovered bugs that could be exploited. This verified BDD implementation can then be used to solve a wide variety of problems with a higher level of confidence than would be possible with an unverified implementation. The formal specification of the Java-based BDD component verified in this project was used to prove the correctness of a reference implementation. Each method in this reference implementation was represented in a reasoning table, and a rigorous set of proofs were written for each verification condition in the reasoning tables. These proofs and the method reasoning tables, taken together, form a single proof that establishes the correctness of the BDD reference implementation as a whole. In the development of formal correctness proofs for each method in the BDD component, several errors in the implementation and specifications were discovered and corrected. These methods had been tested using a comprehensive set of test cases but errors were discovered during the formal verification process, exhibiting the value of the proofs. An additional limitation related to the testing capabilities of the component design pattern used in the Java-based BDD component was also discovered in this work. The results of this thesis mean users can be confident in using this implementation based on its proven correctness.
Paul Sivilotti (Advisor)
Neelam Soundarajan (Committee Member)
297 p.
Computer Science
Formal Verification; Binary Decision Diagram

Recommended Citations

Citations

  • Rumreich, L. (2021). The Binary Decision Diagram: Formal Verification of a Reference Implementation [Master's thesis, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu1618940583868248

    APA Style (7th edition)

  • Rumreich, Laine. The Binary Decision Diagram: Formal Verification of a Reference Implementation. 2021. Ohio State University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=osu1618940583868248.

    MLA Style (8th edition)

  • Rumreich, Laine. "The Binary Decision Diagram: Formal Verification of a Reference Implementation." Master's thesis, Ohio State University, 2021. http://rave.ohiolink.edu/etdc/view?acc_num=osu1618940583868248

    Chicago Manual of Style (17th edition)

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