Induction-Oriented Formal Verification in Symmetric Interconnection Networks

  • Eric Gascard
  • Laurence Pierre
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


The framework of this paper is the formal specification and proof of applications distributed on symmetric interconnection networks, 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 Cayley graph, we model the networks and their communications in the inductive theorem prover Nqthm. 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.


Cayley Graph Interconnection Network Query Point Proof Obligation Matrix Vector Product 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    S. B. Akers and B. Krishnamurthy. A Group Theoretic Model for Symmetric Interconnection Networks. IEEE Transactions on Computers, 38(4), 1989.Google Scholar
  2. [2]
    B.W. Arden and K.W. Tang. Representations and Routing of Cayley Graphs. IEEE Transactions on Communications, 39(11), November 1991.Google Scholar
  3. [3]
    J-C. Bermond, T. Kodate, and S. Perennes. Gossiping in Cayley Graphs by Packets. In Proceedings of Franco-Japanese conference Brest July 95, volume 1120 of Lectures Notes in Computer Science. Springer Verlag, 1996.Google Scholar
  4. [4]
    R. Boyer and J Moore. A Computational Logic Hand-book. Perspectives in Computing, Vol. 23. Academic Press, Inc., 1988.Google Scholar
  5. [5]
    R. Couturier and D. Méry. An experiment in parallelizing an application using formal methods. In CAV’98. LNCS 1427, Springer Verlag, 1998.Google Scholar
  6. [6]
    R. A. Gamboa. Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2. In Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA), 1998.Google Scholar
  7. [7]
    E. Gascard and L. Pierre. Two Approaches to the Formal Proof of Replicated Hardware Systems using the Boyer-Moore Theorem Prover. In Proc. International Workshop on First Order Theorem Provers (FTP’97), October 1997.Google Scholar
  8. [8]
    C. GowriSankaran. Broadcasting on Recursively Decomposable Cayley Graphs. Discrete Applied Mathematics, 53:171–182, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    B. Hendrickson, R. Leland, and S. Plimpton. An Efficient Parallel Algorithm for Matrix-Vector Multiplication. Int. J. High Speed Computing, 7(1):73–88, 1995.CrossRefGoogle Scholar
  10. [10]
    W. H. Hesselink. A mechanical proof of Segall’s PIF algorithm. Formal Aspects of Computing, 9:208–226, 1997.zbMATHCrossRefGoogle Scholar
  11. [11]
    D. Kapur and M. Subramaniam. Automated Reasoning about Parallel Algorithms using Powerlists. In Proc. Algebraic Methodology and Software Technology, AMAST’95, volume 936 of LNCS, pages 416–430. Springer-Verlag, 1995.Google Scholar
  12. [12]
    M. Kaufmann and J S. Moore. An Industrial Strength Theorem prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering, 23(4), April 1997.Google Scholar
  13. [13]
    J. Kornerup. Mapping Powerlists onto Hypercubes. Technical Report TR-94-04, Department of Computer Sciences, University of Texas at Austin, 1994.Google Scholar
  14. [14]
    V. Kumar, A. Grama, A. Gupta, and G. Karypis. Intoduction to Parallel Computing: Design and Analysis of Algorithms. Benjamin Cummings Pub., 1994.Google Scholar
  15. [15]
    T.M. Kurç, C. Aykanet, and B. Özguç. A parallel scaled conjugate-gradient algorithm for the solution phase of gathering radiosity on hypercubes. The Visual Computer, 13(1):1–19, 1997.CrossRefGoogle Scholar
  16. [16]
    Y. Lee, S. Horng, T. Kao, and Y. Chen. Parallel computation of the Euclidean distance transform on the mesh of trees and the hypercube computer. Computer Vision and Image Understanding, 68(1):109–119, October 1997.Google Scholar
  17. [17]
    J. Misra. Powerlist: A structure for parallel recursion. ACM Transactions on Programming Languages and Systems, 16(6):1737–1767, November 1994.Google Scholar
  18. [18]
    J S. Moore. A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213–228, 1999.CrossRefGoogle Scholar
  19. [19]
    K. Qiu and S.G. Akl. Novel Data Communication Algorithms on Hypercubes and Related Interconnection Networks and Their Applications in Computational Geometry. Technical Report 97-415, Department of Computing and Information Science, Queen’s University, Kingston, Ontario, December 1997.Google Scholar
  20. [20]
    M. Snir, S. Otto, S. Huss-Lederman, D. Walker, and J. Dongarra. MPI: The Complete Reference. The MIT Press, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Eric Gascard
    • 1
  • Laurence Pierre
    • 1
  1. 1.LIM - CMI / Universitë de ProvenceMarseille Cedex 13France

Personalised recommendations