Affordable Access

Induction-Oriented Formal Verification in Symmetric Interconnection Networks

IFIP Lecture Notes in Computer Science (LNCS)
Publication Date
  • Communication
  • Computer Science
  • Mathematics


The framework of this paper is the formal specification and proof of , e.g. the torus or the hypercube. The algorithms are distributed over the nodes of the networks and use well-identified communication primitives. Using the notion of , we model the networks and their communications in the inductive theorem prover . Within this environment, we mechanically perform correctness verifications with a specific invariant oriented method. We illustrate our approach with the verification of two distributed algorithms implemented on the hypercube.Full Text at Springer, may require registration or fee

There are no comments yet on this publication. Be the first to share your thoughts.