{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T14:48:47Z","timestamp":1710254927382},"reference-count":13,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Parallel Process. Lett."],"published-print":{"date-parts":[[2003,3]]},"abstract":"<jats:p> This paper focuses on the formal proof of parallel programs dedicated to distributed memory symmetric interconnection networks; communications are realized by message passing. We have developed a method to formally verify the computational correctness of this kind of application. Using the notion of Cayley graphs to model the networks in the Nqthm theorem prover, we have formally specified and mechanically proven correct a large set of collective communication primitives. Our compositional approach allows us to reuse these libraries of pre-proven procedures to validate complex application programs within Nqthm. This is illustrated by three examples. <\/jats:p>","DOI":"10.1142\/s0129626403001094","type":"journal-article","created":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T08:27:11Z","timestamp":1057048031000},"page":"3-18","source":"Crossref","is-referenced-by-count":1,"title":["FORMAL PROOF OF APPLICATIONS DISTRIBUTED IN SYMMETRIC INTERCONNECTION NETWORKS"],"prefix":"10.1142","volume":"13","author":[{"given":"ERIC","family":"GASCARD","sequence":"first","affiliation":[{"name":"LIFO - Universit\u00e9 d'Orl\u00e9ans, BP 6759, 45067 Orl\u00e9ans Cedex 2, France"}]},{"given":"LAURENCE","family":"PIERRE","sequence":"additional","affiliation":[{"name":"I3S - Universit\u00e9 de Nice, BP 121, 06903 Sophia Antipolis Cedex, France"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","volume":"38","author":"Akers S. B.","journal-title":"IEEE Transactions on Computers"},{"key":"rf2","volume":"39","author":"Arden B. W.","journal-title":"IEEE Transactions on Communications"},{"key":"rf4","series-title":"Perspectives in Computing","volume-title":"A Computational Logic Hand-book","volume":"23","author":"Boyer R.","year":"1988"},{"key":"rf5","volume":"16","author":"Chung Kuo-Liang","journal-title":"Pattern Recognition Letters"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(94)90183-X"},{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1142\/S0129053395000051"},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211619"},{"key":"rf14","first-page":"44","volume":"11","author":"Hesselink W. H.","journal-title":"Formal Aspects of Computing"},{"key":"rf16","volume":"23","author":"Kaufmann M.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"rf18","volume-title":"Intoduction to Parallel Computing: Design and Analysis of Algorithms","author":"Kumar V.","year":"1994"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1007\/s003710050085"},{"key":"rf21","volume-title":"Hypercube Algorithms for Image Processing and Pattern Recognition","author":"Ranka S.","year":"1989"},{"key":"rf22","volume-title":"MPI: The Complete Reference","author":"Snir M.","year":"1996"}],"container-title":["Parallel Processing Letters"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129626403001094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T13:33:54Z","timestamp":1565184834000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129626403001094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":13,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2003,3]]}},"alternative-id":["10.1142\/S0129626403001094"],"URL":"https:\/\/doi.org\/10.1142\/s0129626403001094","relation":{},"ISSN":["0129-6264","1793-642X"],"issn-type":[{"value":"0129-6264","type":"print"},{"value":"1793-642X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}