Abstract
The process of showing that a program satisfies some particular properties with respect to its specification is called program verification. Axiomatic semantics is a verification method that makes assertions describing properties about the states of the program. There exists a transformation from the assertions of the verification proof of a program to executable assertions. These executable assertions may be embedded in the program to create a fault-tolerant program. While this approach has been applied to the sequential programming environment, the distributed programming environment presents special challenges. This paper focuses on applying concurrent programming axiomatic proof systems to generate executable assertions in a distributed environment using distributed branch and bound as a model problem.
Recommended Citation
Lutfiyya, Hanan; Sun, Aggie; and McMillin, Bruce M., "Fault-Tolerant Concurrent Branch and Bound Algorithm Derived from Program Verification" (1992). Computer Science Technical Reports. 131.
https://scholarsmine.mst.edu/comsci_techreports/131
Department(s)
Computer Science
Keywords and Phrases
Executable Assertions, Formal Methods, Branch & Bound, Concurrent Program Verification, Fault Tolerance
Report Number
CSc-92-02
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1992 University of Missouri - Rolla, All rights reserved
Publication Date
12 January, 1992
Comments
The first and second Authors are Graduate Students.
This work was supported in part by Ute National Science Foundation under Grant Numbers MIP-8909749 and CDA-8820714, and in part by the AMOCO Faculty Development Program.