A component-based approach to proving the correctness of the Schorr-Waite algorithm

Simple item page
dc.contributor.authorSingh, Amrinderen
dc.contributor.committeechairKulczycki, Gregory W.en
dc.contributor.committeememberLu, Chang-Tienen
dc.contributor.committeememberChen, Ing-Rayen
dc.contributor.departmentComputer Scienceen
dc.date.accessioned2014-03-14T20:44:00Zen
dc.date.adate2007-08-23en
dc.date.available2014-03-14T20:44:00Zen
dc.date.issued2007-08-09en
dc.date.rdate2007-08-23en
dc.date.sdate2007-08-22en
dc.description.abstractThis thesis presents a component-based approach to proving the correctness of programs involving pointers. Unlike previous work, our component-based approach supports modular reasoning, which is essential to the scalability of systems. Specifically, we specify the behavior of a graph-marking algorithm known as the Schorr-Waite algorithm, implement it using a component that captures the behavior and performance benefits of pointers, and prove that the implementation is correct with respect to the specification. We use the Resolve language in our example, which is an integrated programming and specification language that supports modular reasoning. The behavior of the algorithm is fully specified using custom definitions, pre- and post-conditions, and a complex loop invariant. Additional operations for the Resolve pointer component are introduced that preserve the accessibility of a system. These operations are used in the implementation of the algorithm. They simplify the proof of correctness and make the code shorter.en
dc.description.degreeMaster of Scienceen
dc.identifier.otheretd-08222007-151929en
dc.identifier.sourceurlhttp://scholar.lib.vt.edu/theses/available/etd-08222007-151929/en
dc.identifier.urihttp://hdl.handle.net/10919/34702en
dc.publisherVirginia Techen
dc.relation.haspartAmrinder_Singh_Masters_Thesis.pdfen
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subjectmodular reasoningen
dc.subjectmemory managementen
dc.subjectgraph markingen
dc.subjectFormal specificationen
dc.titleA component-based approach to proving the correctness of the Schorr-Waite algorithmen
dc.typeThesisen
thesis.degree.disciplineComputer Scienceen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.levelmastersen
thesis.degree.nameMaster of Scienceen

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Amrinder_Singh_Masters_Thesis.pdf
Size:
418.13 KB
Format:
Adobe Portable Document Format
Download

Collections

Masters Theses