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.

Name thesis:degree_name

Master of Science

Level thesis:degree_level

masters

Discipline thesis:degree_discipline

Computer Science

Department dc:contributor.department

Computer Science

Grantor dc:publisher

Virginia Tech

Year dc:date.issued

2007

Author dc:creator

• Singh, Amrinder

Chair dc:contributor.committeechair

• Kulczycki, Gregory W.

Committee members dc:contributor.committeemember

• Lu, Chang-Tien
• Chen, Ing-Ray

• modular reasoning
• memory management
• graph marking
• Formal specification

Statement dc:rights

• In Copyright

Licence dc:rights.uri

• http://rightsstatements.org/vocab/InC/1.0/

Dc Identifier Other

etd-08222007-151929

OAI identifier oai:identifier

oai:vtechworks.lib.vt.edu:10919/34702