Formalizing Inductive Proofs of Network Algorithms

Dr. Frank Stomp
AT&T Bell Laboratories

Monday, February 19, 1996
11 a.m. - 12 noon
Salisbury Labs 104

Theorem proving and model checking are combined to fully formalize a correctness proof of a broadcasting protocol. The protocol is executed in a network of processors which constitutes a binary tree of arbitrary size. The theorem prover COQ and the model checker SPIN are used to verify the broadcasting protocol.

The goals in this work are twofold. The first one is to provide a strategy for carrying out formal, mechanical correctness proofs of distributed network algorithms. Even though logical specifications of programs implementing such algorithms are often defined precisely enough to allow a human verifier to prove the program's correctness, the definition of the network is often only informal or implicit. The example illustrates how an underlying network can be formally defined by means of induction, and how to reason about network algorithms by structural induction. The second goal is to integrate theorem proving and model checking to increase the class of algorithms for which mechanical verification is practical. Theorem provers are expressive and powerful, but require sophisticated insight and guidance by the user. Model checkers are fully automatic and effective for verifying finite state automata, but limited to finite spaces of a certain size. I will provide a proof strategy which draws on the strengths of both techniques.

(Joint work with Ramesh Bharadwaj, CRL, McMaster University, and Amy Felty, AT&T Bell Laboratories.)

Maintained by webmaster@wpi.edu
Last modified: Sep 27, 2006, 16:05 EDT