--- _id: '1392' abstract: - lang: eng text: Fault-tolerant distributed algorithms play an important role in ensuring the reliability of many software applications. In this paper we consider distributed algorithms whose computations are organized in rounds. To verify the correctness of such algorithms, we reason about (i) properties (such as invariants) of the state, (ii) the transitions controlled by the algorithm, and (iii) the communication graph. We introduce a logic that addresses these points, and contains set comprehensions with cardinality constraints, function symbols to describe the local states of each process, and a limited form of quantifier alternation to express the verification conditions. We show its use in automating the verification of consensus algorithms. In particular, we give a semi-decision procedure for the unsatisfiability problem of the logic and identify a decidable fragment. We successfully applied our framework to verify the correctness of a variety of consensus algorithms tolerant to both benign faults (message loss, process crashes) and value faults (message corruption). acknowledgement: Supported by the Vienna Science and Technology Fund (WWTF) through grant PROSEED. alternative_title: - LNCS author: - first_name: Cezara full_name: Dragoi, Cezara id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87 last_name: Dragoi - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Helmut full_name: Veith, Helmut last_name: Veith - first_name: Josef full_name: Widder, Josef last_name: Widder - first_name: Damien full_name: Zufferey, Damien id: 4397AC76-F248-11E8-B48F-1D18A9856A87 last_name: Zufferey orcid: 0000-0002-3197-8736 citation: ama: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:10.1007/978-3-642-54013-4_10' apa: 'Dragoi, C., Henzinger, T. A., Veith, H., Widder, J., & Zufferey, D. (2014). A logic-based framework for verifying consensus algorithms (Vol. 8318, pp. 161–181). Presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA: Springer. https://doi.org/10.1007/978-3-642-54013-4_10' chicago: Dragoi, Cezara, Thomas A Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. “A Logic-Based Framework for Verifying Consensus Algorithms,” 8318:161–81. Springer, 2014. https://doi.org/10.1007/978-3-642-54013-4_10. ieee: 'C. Dragoi, T. A. Henzinger, H. Veith, J. Widder, and D. Zufferey, “A logic-based framework for verifying consensus algorithms,” presented at the VMCAI: Verification, Model Checking and Abstract Interpretation, San Diego, USA, 2014, vol. 8318, pp. 161–181.' ista: 'Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. 2014. A logic-based framework for verifying consensus algorithms. VMCAI: Verification, Model Checking and Abstract Interpretation, LNCS, vol. 8318, 161–181.' mla: Dragoi, Cezara, et al. A Logic-Based Framework for Verifying Consensus Algorithms. Vol. 8318, Springer, 2014, pp. 161–81, doi:10.1007/978-3-642-54013-4_10. short: C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181. conference: end_date: 2014-01-21 location: San Diego, USA name: 'VMCAI: Verification, Model Checking and Abstract Interpretation' start_date: 2014-01-19 date_created: 2018-12-11T11:51:45Z date_published: 2014-01-01T00:00:00Z date_updated: 2021-01-12T06:50:22Z day: '01' ddc: - '000' - '005' department: - _id: ToHe doi: 10.1007/978-3-642-54013-4_10 ec_funded: 1 file: - access_level: open_access checksum: bffa33d39be77df0da39defe97eabf84 content_type: application/pdf creator: system date_created: 2018-12-12T10:11:06Z date_updated: 2020-07-14T12:44:48Z file_id: '4859' file_name: IST-2014-179-v1+1_vmcai14.pdf file_size: 444138 relation: main_file file_date_updated: 2020-07-14T12:44:48Z has_accepted_license: '1' intvolume: ' 8318' language: - iso: eng month: '01' oa: 1 oa_version: Submitted Version page: 161 - 181 project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication_status: published publisher: Springer publist_id: '5817' pubrep_id: '179' quality_controlled: '1' scopus_import: 1 status: public title: A logic-based framework for verifying consensus algorithms type: conference user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 8318 year: '2014' ...