Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


Merten.pdf (301.1 KB)

ETD Abstract Container

Abstract Header

A Verified Program for the Enumeration of All Maximal Independent Sets

Merten, Samuel A.
http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1479829000576398

Abstract Details

2016, Master of Science (MS), Ohio University, Computer Science (Engineering and Technology).
Errors in programs and mathematical results are a common cause for wasted time and resources. While peer-review and software-engineering techniques are helpful in mitigating the occurrence of these errors, the human element at the center of these techniques is fallible, and for very large or complex results the application of these techniques is often infeasible. Towards this end, researchers have developed a number of tools, proof assistants, which aid the user in constructing machine-checkable formal proofs. Tools and theories verified using these tools carry a much stronger assurance of correctness than many alternatives. Currently, a number of fundamental theorems and programs have been proven correct within these proof assistants, as well as a number of proofs which were previously deemed too large for review. However, despite these successes, and the ubiquity of graph algorithms in computer science, little work has been done towards generating verified implementations of graph algorithms. This thesis describes my attempt to address this weakness through the construction of a verified implementation of Tsukiyama et al.’s algorithm for enumerating all maximal independent sets of a graph. The enumeration of all maximal independent sets has a number of immediate applications in domains such as computer vision, computational chemistry and information systems, as well as being an important subroutine in efficient algorithms for exact graph coloring. Such a verified algorithm could lay the foundation for a library of verified graph algorithms suitable for use in critical systems.
David Juedes, PhD. (Advisor)
Gordon Stewart, PhD. (Committee Member)
Chang Liu, PhD. (Committee Member)
Archil Gulisashvili , PhD. (Committee Member)
59 p.
Computer Science
software verification; proof assistants; graph theory; independent sets

Recommended Citations

Citations

  • Merten, S. A. (2016). A Verified Program for the Enumeration of All Maximal Independent Sets [Master's thesis, Ohio University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1479829000576398

    APA Style (7th edition)

  • Merten, Samuel. A Verified Program for the Enumeration of All Maximal Independent Sets. 2016. Ohio University, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1479829000576398.

    MLA Style (8th edition)

  • Merten, Samuel. "A Verified Program for the Enumeration of All Maximal Independent Sets." Master's thesis, Ohio University, 2016. http://rave.ohiolink.edu/etdc/view?acc_num=ohiou1479829000576398

    Chicago Manual of Style (17th edition)

ohiou1479829000576398
787
© 2016, all rights reserved.
This open access ETD is published by Ohio University and OhioLINK.