{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T19:40:02Z","timestamp":1748979602067,"version":"3.41.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319395692"},{"type":"electronic","value":"9783319395708"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-39570-8_3","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:04:10Z","timestamp":1464066250000},"page":"36-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Framework for Certified Self-Stabilization"],"prefix":"10.1007","author":[{"given":"Karine","family":"Altisen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Corbineau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Devismes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.jocs.2012.01.003","volume":"4","author":"J Ben-Othman","year":"2013","unstructured":"Ben-Othman, J., Bessaoud, K., Bui, A., Pilard, L.: Self-stabilizing algorithm for efficient topology control in wireless sensor networks. J. Comput. Sci. 4(4), 199\u2013208 (2013)","journal-title":"J. Comput. Sci."},{"issue":"4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1017\/S0960129511000120","volume":"21","author":"F Blanqui","year":"2011","unstructured":"Blanqui, F., Koprowski, A.: CoLoR: a coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827\u2013859 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"6","key":"3_CR3","doi-asserted-by":"publisher","first-page":"1533","DOI":"10.1016\/j.future.2012.10.003","volume":"29","author":"E Caron","year":"2013","unstructured":"Caron, E., Chuffart, F., Tedeschi, C.: When self-stabilization meets real platforms: an experimental study of a peer-to-peer service discovery system. future gener. comput. syst. 29(6), 1533\u20131543 (2013)","journal-title":"future gener. comput. syst."},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Chen, M., Monin, J.F.: Formal verification of netlog protocols. In: TASE (2012)","DOI":"10.1109\/TASE.2012.19"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/0020-0190(91)90111-T","volume":"39","author":"N Chen","year":"1991","unstructured":"Chen, N., Yu, H., Huang, S.: A self-stabilizing algorithm for constructing spanning trees. Inf. Process. Lett. 39, 147\u2013151 (1991)","journal-title":"Inf. Process. Lett."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Courtieu, P.: Proving self-stabilization with a proof assistant. In: IPDPS (2002)","DOI":"10.1109\/IPDPS.2002.1016619"},{"issue":"3","key":"3_CR7","doi-asserted-by":"publisher","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":"3_CR8","doi-asserted-by":"crossref","unstructured":"Datta, A.K., Larmore, L.L., Devismes, S., Heurtefeux, K., Rivierre, Y.: Competitive self-stabilizing k-clustering. In: ICDCS (2012)","DOI":"10.1109\/ICDCS.2012.72"},{"issue":"1","key":"3_CR9","doi-asserted-by":"crossref","first-page":"116","DOI":"10.15803\/ijnc.3.1_116","volume":"3","author":"AK Datta","year":"2013","unstructured":"Datta, A.K., Larmore, L.L., Devismes, S., Heurtefeux, K., Rivierre, Y.: Self-stabilizing small k-dominating sets. IJNC 3(1), 116\u2013136 (2013)","journal-title":"IJNC"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Deng, Y., Monin, J.F.: Verifying self-stabilizing population protocols with Coq. In: TASE (2009)","DOI":"10.1109\/TASE.2009.9"},{"issue":"8","key":"3_CR11","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Dolev, S., Gouda, M.G., Schneider, M.: Memory requirements for silent stabilization. In: PODC, pp. 27\u201334 (1996)","DOI":"10.1145\/248052.248055"},{"issue":"4","key":"3_CR14","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1145\/155183.155228","volume":"15","author":"S Ghosh","year":"1993","unstructured":"Ghosh, S.: An alternative solution to a problem on self-stabilization. ACM Trans. Program. Lang. Syst. 15(4), 735\u2013742 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF02278857","volume":"7","author":"S Huang","year":"1993","unstructured":"Huang, S., Chen, N.: Self-stabilizing depth-first token circulation on networks. Distrib. Comput. 7(1), 61\u201366 (1993)","journal-title":"Distrib. Comput."},{"key":"3_CR16","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., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209\u2013224. Springer, Heidelberg (2012)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Rushby, J.M., Shankar, N.: A case-study in component-based mechanical verification of fault-tolerant programs. In: WSS, pp. 33\u201340 (1999)","DOI":"10.1109\/SLFSTB.1999.777484"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","volume":"11","author":"L Lamport","year":"2012","unstructured":"Lamport, L.: How to write a 21st century proof. J. fixed point theory appl. 11(1), 43\u201363 (2012)","journal-title":"J. fixed point theory appl."},{"key":"3_CR19","unstructured":"The Coq Development Team: The Coq Proof Assistant, Reference Manual. http:\/\/coq.inria.fr\/refman\/"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-39570-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T19:05:40Z","timestamp":1748977540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-39570-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319395692","9783319395708"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-39570-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"24 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}