Return to search

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

This 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. / Master of Science

Identiferoai:union.ndltd.org:VTETD/oai:vtechworks.lib.vt.edu:10919/34702
Date23 August 2007
CreatorsSingh, Amrinder
ContributorsComputer Science, Kulczycki, Gregory W., Lu, Chang-Tien, Chen, Ing-Ray
PublisherVirginia Tech
Source SetsVirginia Tech Theses and Dissertation
Detected LanguageEnglish
TypeThesis
Formatapplication/pdf
RightsIn Copyright, http://rightsstatements.org/vocab/InC/1.0/
RelationAmrinder_Singh_Masters_Thesis.pdf

Page generated in 0.0022 seconds