{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:03:42Z","timestamp":1725865422073},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_5","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:11:57Z","timestamp":1474409517000},"page":"69-81","source":"Crossref","is-referenced-by-count":0,"title":["Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Allyx","family":"Fontaine","sequence":"first","affiliation":[]},{"given":"Akka","family":"Zemmari","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"issue":"8","key":"5_CR1","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"5_CR2","first-page":"39","volume":"9","author":"P Cast\u00e9ran","year":"2011","unstructured":"Cast\u00e9ran, P., Filou, V.: Tasks, types and tactics for local computation systems. Studia Informatica Universalis 9(1), 39\u201386 (2011)","journal-title":"Studia Informatica Universalis"},{"issue":"2","key":"5_CR3","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1093\/comjnl\/38.2.152","volume":"38","author":"CT Chou","year":"1995","unstructured":"Chou, C.T.: Mechanical verification of distributed algorithms in higher-order logic. Comput. J. 38(2), 152\u2013161 (1995)","journal-title":"Comput. J."},{"issue":"3","key":"5_CR4","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1016\/j.ipl.2014.11.001","volume":"115","author":"P Courtieu","year":"2015","unstructured":"Courtieu, P., Rieg, L., Tixeuil, S., Urbain, X.: Impossibility of gathering, a certification. Inf. Process. Lett. 115(3), 447\u2013452 (2015)","journal-title":"Inf. Process. Lett."},{"key":"5_CR5","series-title":"Mathematics in Science and Engineering","volume-title":"Finite State Markovian Decision Processes","author":"C Derman","year":"1970","unstructured":"Derman, C.: Finite State Markovian Decision Processes. Mathematics in Science and Engineering. Academic Press, Orlando (1970)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Deng, Y., Monin, J.F.: Verifying self-stabilizing population protocols with Coq. In: TASE, pp. 201\u2013208 (2009)","DOI":"10.1109\/TASE.2009.9"},{"key":"5_CR7","unstructured":"Fontaine, A., Zemmari, A.: RDA: a Coq Library on Randomised Distributed Algorithms. http:\/\/www.allyxfontaine.com\/RDA"},{"key":"5_CR8","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2008)"},{"key":"5_CR9","unstructured":"http:\/\/www.haskell.org\/haskellwiki\/monad"},{"key":"5_CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/j.entcs.2004.01.021","volume":"112","author":"J Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in ol. Electr. Notes Theor. Comput. Sci. 112, 95\u2013111 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Prism: probabilistic symbolic model checker. In: Computer Performance Evaluation\/TOOLS, pp. 200\u2013204 (2002)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-33475-7_15","volume-title":"Theoretical Computer Science","author":"P K\u00fcfner","year":"2012","unstructured":"K\u00fcfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33475-7_15"},{"key":"5_CR13","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"MZ Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-21437-0_26","volume-title":"FM 2011: Formal Methods","author":"D M\u00e9ry","year":"2011","unstructured":"M\u00e9ry, D., Mosbah, M., Tounsi, M.: Refinement-based verification of local synchronization algorithms. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 338\u2013352. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21437-0_26"},{"issue":"1","key":"5_CR15","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0890-5401(03)00054-3","volume":"184","author":"Y M\u00e9tivier","year":"2003","unstructured":"M\u00e9tivier, Y., Saheb, N., Zemmari, A.: Analysis of a randomized rendezvous algorithm. Inf. Comput. 184(1), 109\u2013128 (2003)","journal-title":"Inf. Comput."},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Pogosyants, A., Segala, R.: Formal verification of timed properties for randomized distributed algorithms. In: PODC, pp. 174\u2013183 (1995)","DOI":"10.1145\/224964.224984"},{"key":"5_CR17","unstructured":"\u201cCoq Development Team\u201d. The Coq Proof Assistant Reference Manual. coq.inria.fr"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:17:20Z","timestamp":1498331840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}