A mechanical proof of Segall's PIF algorithm

1 March 1997

journal article
research article
Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing

Vol. 9 (2) , 208-226
https://doi.org/10.1007/bf01211619

Abstract

We describe the construction of a distributed algorithm with asynchronous communication together with a mechanically verified proof of correctness. For this purpose we treat Segall's PIF algorithm (propagation of information with feedback). The proofs are based on invariants, and variant functions for termination. The theorem prover NQTHM is used to deal with the many case distinctions due to asynchronous distributed computation. Emphasis is on the modelling assumptions, the treatment of nondeterminacy, the forms of termination detection, and the proof obligations for a complete mechanical proof. Finally, a comparison is made with (the proof of) the minimum spanning tree algorithm of Gallager, Humblet, and Spira, for which the technique was developed.

Keywords

This publication has 14 references indexed in Scilit:

The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract
Formal Aspects of Computing, 1999
Verification of a distributed summation algorithm
Published by Springer Nature ,1995
Mechanical verification of distributed algorithms in higher-order logic
The Computer Journal, 1995
Receptive process theory
Acta Informatica, 1992
Multivalued Possibilities Mappings
Published by Defense Technical Information Center (DTIC) ,1990
Multivalued possibilities mappings
Published by Springer Nature ,1990
Parallel Program Design
Published by Springer Nature ,1989
A Lattice-Structured Proof Technique Applied to a Minimum Spanning Tree Algorithm
Published by Defense Technical Information Center (DTIC) ,1988
Distributed network protocols
IEEE Transactions on Information Theory, 1983
An axiomatic proof technique for parallel programs I
Acta Informatica, 1976