{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:20Z","timestamp":1760202680302},"reference-count":0,"publisher":"National Library of Serbia","issue":"1","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>The snapshot problem addresses a collection of important algorithmic issues\n   related to distributed computations, which are used for debugging or\n   recovering distributed programs. Among existing solutions, Chandy and Lamport\n   have proposed a simple distributed algorithm. In this paper, we explore the\n   correct-byconstruction process to formalize the snapshot algorithms in\n   distributed system. The formalization process is based on a modeling language\n   Event B, which supports a refinement-based incremental development using\n   RODIN platform. These refinement-based techniques help to derive correct\n   distributed algorithms. Moreover, we demonstrate how other distributed\n   algorithms can be revisited. A consequence is to provide a fully mechanized\n   proof of the resulting distributed algorithms.<\/jats:p>","DOI":"10.2298\/csis130122007a","type":"journal-article","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T11:37:09Z","timestamp":1388749029000},"page":"251-270","source":"Crossref","is-referenced-by-count":16,"title":["Revisiting snapshot algorithms by refinement-based techniques"],"prefix":"10.2298","volume":"11","author":[{"suffix":"Manamiary","given":"Bruno","family":"Andriamiarina","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, LORIA Vandoeuvre-l\u00e8s-Nancy, France"}]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, LORIA Vandoeuvre-l\u00e8s-Nancy, France"}]},{"suffix":"Neeraj","given":"Kumar","family":"Singh","sequence":"additional","affiliation":[{"name":"McMaster Centre for Software Certification, McMaster University Hamilton, Ontario, Canada"}]}],"member":"1078","container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:31:18Z","timestamp":1685349078000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02141400007A"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014]]}},"URL":"https:\/\/doi.org\/10.2298\/csis130122007a","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}