A Synthesized Algorithm for Interactive Consistency

Adrià Gascón, Ashish Tiwari

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We revisit the interactive consistency problem introduced by Pease, Shostak and Lamport. We first show that their algorithm does not achieve interactive consistency if faults are transient, even if faults are non-malicious. We then present an algorithm that achieves interactive consistency in the presence of non-malicious, asymmetric and transient faults, but only under an additional guaranteed delayed ack assumption. We discovered our algorithm using an automated synthesis technique that is based on bounded model checking and QBF solving. Our synthesis technique is general and simple, and it is a promising approach for synthesizing distributed algorithms.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication6th International Symposium, NFM 2014, Houston, TX, USA, April 29 – May 1, 2014. Proceedings
EditorsJulia M. Badger, Kristin Yvonne Rozier
PublisherSpringer International Publishing
Number of pages15
ISBN (Electronic)978-3-319-06200-6
ISBN (Print)978-3-319-06199-3
Publication statusPublished - 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'A Synthesized Algorithm for Interactive Consistency'. Together they form a unique fingerprint.

Cite this