{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:01:50Z","timestamp":1725483710728},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_32","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T13:16:15Z","timestamp":1178198175000},"page":"418-432","source":"Crossref","is-referenced-by-count":1,"title":["Induction-Oriented Formal Verification in Symmetric Interconnection Networks"],"prefix":"10.1007","author":[{"given":"Eric","family":"Gascard","sequence":"first","affiliation":[]},{"given":"Laurence","family":"Pierre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"S. B. Akers and B. Krishnamurthy. A Group Theoretic Model for Symmetric Interconnection Networks. IEEE Transactions on Computers, 38(4), 1989.","DOI":"10.1109\/12.21148"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"B.W. Arden and K.W. Tang. Representations and Routing of Cayley Graphs. IEEE Transactions on Communications, 39(11), November 1991.","DOI":"10.1109\/26.111428"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-61576-8_91"},{"key":"32_CR4","unstructured":"R. Boyer and J Moore. A Computational Logic Hand-book. Perspectives in Computing, Vol. 23. Academic Press, Inc., 1988."},{"key":"32_CR5","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201998","author":"R. Couturier","year":"1998","unstructured":"R. Couturier and D. M\u00e9ry. An experiment in parallelizing an application using formal methods. In CAV\u201998. LNCS 1427, Springer Verlag, 1998."},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-64359-1_743"},{"key":"32_CR7","unstructured":"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\u201997), October 1997."},{"key":"32_CR8","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/0166-218X(94)90183-X","volume":"53","author":"C. GowriSankaran","year":"1994","unstructured":"C. GowriSankaran. Broadcasting on Recursively Decomposable Cayley Graphs. Discrete Applied Mathematics, 53:171\u2013182, 1994.","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"32_CR9","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1142\/S0129053395000051","volume":"7","author":"B. Hendrickson","year":"1995","unstructured":"B. Hendrickson, R. Leland, and S. Plimpton. An Efficient Parallel Algorithm for Matrix-Vector Multiplication. Int. J. High Speed Computing, 7(1):73\u201388, 1995.","journal-title":"Int. J. High Speed Computing"},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BF01211619","volume":"9","author":"W. H. Hesselink","year":"1997","unstructured":"W. H. Hesselink. A mechanical proof of Segall\u2019s PIF algorithm. Formal Aspects of Computing, 9:208\u2013226, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"32_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/3-540-60043-4_68","volume-title":"Proc. Algebraic Methodology and Software Technology, AMAST\u201995","author":"D. Kapur","year":"1995","unstructured":"D. Kapur and M. Subramaniam. Automated Reasoning about Parallel Algorithms using Powerlists. In Proc. Algebraic Methodology and Software Technology, AMAST\u201995, volume 936 of LNCS, pages 416\u2013430. Springer-Verlag, 1995."},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/32.588534"},{"key":"32_CR13","unstructured":"J. Kornerup. Mapping Powerlists onto Hypercubes. Technical Report TR-94-04, Department of Computer Sciences, University of Texas at Austin, 1994."},{"key":"32_CR14","unstructured":"V. Kumar, A. Grama, A. Gupta, and G. Karypis. Intoduction to Parallel Computing: Design and Analysis of Algorithms. Benjamin Cummings Pub., 1994."},{"issue":"1","key":"32_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s003710050085","volume":"13","author":"T.M. Kur\u00e7","year":"1997","unstructured":"T.M. Kur\u00e7, C. Aykanet, and B. \u00d6zgu\u00e7. A parallel scaled conjugate-gradient algorithm for the solution phase of gathering radiosity on hypercubes. The Visual Computer, 13(1):1\u201319, 1997.","journal-title":"The Visual Computer"},{"issue":"1","key":"32_CR16","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1006\/cviu.1997.0539","volume":"68","author":"Y. Lee","year":"1997","unstructured":"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\u2013119, October 1997.","journal-title":"Computer Vision and Image Understanding"},{"issue":"6","key":"32_CR17","doi-asserted-by":"crossref","first-page":"1737","DOI":"10.1145\/197320.197356","volume":"16","author":"J. Misra","year":"1994","unstructured":"J. Misra. Powerlist: A structure for parallel recursion. ACM Transactions on Programming Languages and Systems, 16(6):1737\u20131767, November 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"32_CR18","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1023\/A:1008624904634","volume":"14","author":"J. S. Moore","year":"1999","unstructured":"J S. Moore. A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213\u2013228, 1999.","journal-title":"Formal Methods in System Design"},{"key":"32_CR19","volume-title":"Technical Report 97-415","author":"K. Qiu","year":"1997","unstructured":"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\u2019s University, Kingston, Ontario, December 1997."},{"key":"32_CR20","unstructured":"M. Snir, S. Otto, S. Huss-Lederman, D. Walker, and J. Dongarra. MPI: The Complete Reference. The MIT Press, 1996."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T07:46:57Z","timestamp":1550303217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}