{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:56:30Z","timestamp":1761807390396,"version":"3.41.0"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2007,10]]},"abstract":"<jats:p>We give a survey of formal verification techniques that can be used to corroborate existing experimental results for gossiping protocols in a rigorous manner. We present properties of interest for gossiping protocols and discuss how various formal evaluation techniques can be employed to predict them.<\/jats:p>","DOI":"10.1145\/1317379.1317385","type":"journal-article","created":{"date-parts":[[2007,11,16]],"date-time":"2007-11-16T15:57:07Z","timestamp":1195228627000},"page":"28-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Formal analysis techniques for gossiping protocols"],"prefix":"10.1145","volume":"41","author":[{"given":"Rena","family":"Bakhshi","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francois","family":"Bonnet","sequence":"additional","affiliation":[{"name":"ENS Cachan\/IRISA, Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wan","family":"Fokkink","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boudewijn","family":"Haverkort","sequence":"additional","affiliation":[{"name":"University of Twente, Enschede, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073814.1073871"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.242"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.36"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.733948"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_6_1","volume-title":"Mathematical Theory of Infectious Diseases and Its Applications","author":"Bailey N. T.","year":"1975","unstructured":"N. T. Bailey . Mathematical Theory of Infectious Diseases and Its Applications . Griffin , London , second edition, 1975 . N. T. Bailey. Mathematical Theory of Infectious Diseases and Its Applications. Griffin, London, second edition, 1975."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132905.1132932"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems: Proc. 4th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-RT","author":"Behrmann G.","year":"2004","unstructured":"G. Behrmann , A. David , and K. G. Larsen . A tutorial on uppaal . In Formal Methods for the Design of Real-Time Systems: Proc. 4th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-RT 2004 ), number 3185 in LNCS, pages 200 -- 236 . Springer , 2004. G. Behrmann, A. David, and K. G. Larsen. A tutorial on uppaal. In Formal Methods for the Design of Real-Time Systems: Proc. 4th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-RT 2004), number 3185 in LNCS, pages 200--236. Springer, 2004."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0129-2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0007-0"},{"key":"e_1_2_1_11_1","series-title":"Texts in Theoretical Computer Science: An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions , volume XXV of Texts in Theoretical Computer Science: An EATCS Series . Springer , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, volume XXV of Texts in Theoretical Computer Science: An EATCS Series. Springer, 2004."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/312203.312207"},{"key":"e_1_2_1_13_1","first-page":"2","volume-title":"Performance analysis of Cyclon, an inexpensive membership management for unstructured","author":"Bonnet F.","year":"2006","unstructured":"F. Bonnet . Performance analysis of Cyclon, an inexpensive membership management for unstructured p 2 p overlays. Master thesis, ENS Cachan Bretagne, University of Rennes , IRISA, 2006 . F. Bonnet. Performance analysis of Cyclon, an inexpensive membership management for unstructured p2p overlays. Master thesis, ENS Cachan Bretagne, University of Rennes, IRISA, 2006."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.35"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498447"},{"key":"e_1_2_1_16_1","first-page":"240","volume-title":"Proc. 7th Workshop on Algorithm Eng. and Experiments and 2nd Workshop on Analytic Algorithmics and Combinatorics (ALENEX\/ANALCO 2005","author":"Boyd S.","year":"2005","unstructured":"S. Boyd , A. Ghosh , B. Prabhakar , and D. Shah . Mixing times for random walks on geometric random graphs . In Proc. 7th Workshop on Algorithm Eng. and Experiments and 2nd Workshop on Analytic Algorithmics and Combinatorics (ALENEX\/ANALCO 2005 ), pages 240 -- 249 . SIAM, 2005 . S. Boyd, A. Ghosh, B. Prabhakar, and D. Shah. Mixing times for random walks on geometric random graphs. In Proc. 7th Workshop on Algorithm Eng. and Experiments and 2nd Workshop on Analytic Algorithmics and Combinatorics (ALENEX\/ANALCO 2005), pages 240--249. SIAM, 2005."},{"key":"e_1_2_1_17_1","volume-title":"Proc. 6th Int. Workshop on Automated Verification of Critical Syst (AVoCS'06)","author":"Cadilhac M.","year":"2006","unstructured":"M. Cadilhac , T. H\u00e9rault , R. Lassaigne , S. Peyronnet , and S. Tixeuil . Evaluating complex MAC protocols for sensor networks with APMC . In Proc. 6th Int. Workshop on Automated Verification of Critical Syst (AVoCS'06) , ENTCS. Elsevier , 2006 . To appear. M. Cadilhac, T. H\u00e9rault, R. Lassaigne, S. Peyronnet, and S. Tixeuil. Evaluating complex MAC protocols for sensor networks with APMC. In Proc. 6th Int. Workshop on Automated Verification of Critical Syst (AVoCS'06), ENTCS. Elsevier, 2006. To appear."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/584490.584499"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-540-72522-0_4","volume-title":"Formal Methods for the Performance Evaluation: Proc. 7th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-PE","author":"Clark A.","year":"2007","unstructured":"A. Clark , S. Gilmore , J. Hillston , and M. Tribastone . Stochastic process algebra . In Formal Methods for the Performance Evaluation: Proc. 7th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-PE 2007 ), number 4486 in LNCS, pages 132 -- 179 . Springer , 2007. A. Clark, S. Gilmore, J. Hillston, and M. Tribastone. Stochastic process algebra. In Formal Methods for the Performance Evaluation: Proc. 7th Int. School on Formal Methods for the Design of Comput., Commun. and Software Syst. (SFM-PE 2007), number 4486 in LNCS, pages 132--179. Springer, 2007."},{"key":"e_1_2_1_21_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"2000","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . MIT Press , 2000 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539797315306"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.2006.874532"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/RIVF.2006.1696417"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.27"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41841"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127777.1127791"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1272366.1272386"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/945506.945507"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2004.1297243"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2090188.2090204"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52921-7_62"},{"key":"e_1_2_1_33_1","series-title":"Springer Series in Operations Research","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2553-7","volume-title":"Monte Carlo: Concepts, Algorithms, and Applications","author":"Fishman G. S.","year":"1996","unstructured":"G. S. Fishman . Monte Carlo: Concepts, Algorithms, and Applications . Springer Series in Operations Research . Springer , 1996 . G. S. Fishman. Monte Carlo: Concepts, Algorithms, and Applications. Springer Series in Operations Research. Springer, 1996."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498374"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/648089.747488"},{"key":"e_1_2_1_36_1","first-page":"59","volume-title":"Steen. A Gossip-based Distributed News Service for Wireless Mesh Networks. In Proc. 3rd IEEE Conf. on Wireless On demand Network Syst. and Services (WONS'06)","author":"Gavidia D.","year":"2006","unstructured":"D. Gavidia , S. Voulgaris , and M. van Steen. A Gossip-based Distributed News Service for Wireless Mesh Networks. In Proc. 3rd IEEE Conf. on Wireless On demand Network Syst. and Services (WONS'06) , pages 59 -- 67 . IEEE Computer Society , 2006 . D. Gavidia, S. Voulgaris, and M. van Steen. A Gossip-based Distributed News Service for Wireless Mesh Networks. In Proc. 3rd IEEE Conf. on Wireless On demand Network Syst. and Services (WONS'06), pages 59--67. IEEE Computer Society, 2006."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.016"},{"issue":"1","key":"e_1_2_1_39_1","first-page":"23","volume":"16","author":"Hammersley J. M.","year":"1954","unstructured":"J. M. Hammersley and K. W. Morton . Poor Man's Monte Carlo. J. Royal Statistical Soc. Series B (Methodological) , 16 ( 1 ): 23 -- 38 , 1954 . J. M. Hammersley and K. W. Morton. Poor Man's Monte Carlo. J. Royal Statistical Soc. Series B (Methodological), 16(1):23--38, 1954.","journal-title":"Poor Man's Monte Carlo. J. Royal Statistical Soc. Series B (Methodological)"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_41_1","first-page":"501","volume-title":"Proc. Int. Workshop on Process Algebra and Performance Modeling","volume":"1853","author":"Haverkort B. R.","year":"2000","unstructured":"B. R. Haverkort . Are stochastic process algebras good for performance and dependability evaluation . In Proc. Int. Workshop on Process Algebra and Performance Modeling , volume 1853 of LNCS, pages 501 -- 510 . Springer , 2000 . B. R. Haverkort. Are stochastic process algebras good for performance and dependability evaluation. In Proc. Int. Workshop on Process Algebra and Performance Modeling, volume 1853 of LNCS, pages 501--510. Springer, 2000."},{"key":"e_1_2_1_42_1","series-title":"LNCS","first-page":"38","volume-title":"European Educ. Forum: School on Formal Methods and Performance Analysis","author":"Haverkort B. R.","year":"2002","unstructured":"B. R. Haverkort . Markovian models for performance and dependability evaluation . In European Educ. Forum: School on Formal Methods and Performance Analysis , volume 2090 of LNCS , pages 38 -- 83 . Springer , 2002 . B. R. Haverkort. Markovian models for performance and dependability evaluation. In European Educ. Forum: School on Formal Methods and Performance Analysis, volume 2090 of LNCS, pages 38--83. Springer, 2002."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/829525.831103"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"e_1_2_1_46_1","volume-title":"The Spin Model Checker, Primer and Reference Manual","author":"Holzmann G.","year":"2003","unstructured":"G. Holzmann . The Spin Model Checker, Primer and Reference Manual . Addison-Wesley , 2003 . G. Holzmann. The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, 2003."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2491-2_5"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/975331"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/1045658.1045666"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/795666.796561"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763519"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770401"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/946243.946317"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/380752.380796"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/645413.652161"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.19"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664575"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2003.1209243"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISoLA.2006.51"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146381.1146401"},{"key":"e_1_2_1_61_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0062-0"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.5555\/647765.735995"},{"key":"e_1_2_1_64_1","first-page":"1","article-title":"Tribler: A social-based peer-to-peer system","volume":"19","author":"Pouwelse J.","year":"2007","unstructured":"J. Pouwelse , P. Garbacki , J. Wang , A. Bakker , J. Yang , A. Iosup , D. Epema , M. Reinders , M. van Steen , and H. Sips . Tribler: A social-based peer-to-peer system . Concurrency and Computation: Practice and Experience , 19 : 1 -- 11 , 2007 . J. Pouwelse, P. Garbacki, J. Wang, A. Bakker, J. Yang, A. Iosup, D. Epema, M. Reinders, M. van Steen, and H. Sips. Tribler: A social-based peer-to-peer system. Concurrency and Computation: Practice and Experience, 19:1--11, 2007.","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman M. L.","year":"1994","unstructured":"M. L. Puterman . Markov Decision Processes: Discrete Stochastic Dynamic Programming . John Wiley & amp; Sons, Inc., New York, NY, USA, 1994 . M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley &amp; Sons, Inc., New York, NY, USA, 1994."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2006.30"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24611-4_13"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/762483.762485"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/1659232.1659238"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/774763.774784"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10922-005-4441-x"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0187-8"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.760735"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1317379.1317385","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1317379.1317385","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:39:17Z","timestamp":1750253957000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1317379.1317385"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":73,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["10.1145\/1317379.1317385"],"URL":"https:\/\/doi.org\/10.1145\/1317379.1317385","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2007,10]]},"assertion":[{"value":"2007-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}