000171619 001__ 171619
000171619 005__ 20190316235240.0
000171619 0247_ $$2doi$$a10.1007/s00446-010-0123-3
000171619 022__ $$a0178-2770
000171619 02470 $$2ISI$$a000288716600004
000171619 037__ $$aARTICLE
000171619 245__ $$aVerification of consensus algorithms using satisfiability solving
000171619 269__ $$a2011
000171619 260__ $$bSpringer Verlag$$c2011
000171619 336__ $$aJournal Articles
000171619 520__ $$aConsensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.
000171619 6531_ $$aConsensus
000171619 6531_ $$aModel checking
000171619 6531_ $$aFault-tolerant distributed algorithms
000171619 6531_ $$aFormal verification
000171619 6531_ $$aBounded Model Checking
000171619 6531_ $$aDistributed Consensus
000171619 6531_ $$aAutomated Verification
000171619 6531_ $$aAgreement
000171619 6531_ $$aInduction
000171619 6531_ $$aSystems
000171619 6531_ $$aSolver
000171619 6531_ $$aPaxos
000171619 6531_ $$aTime
000171619 700__ $$aTsuchiya, Tatsuhiro
000171619 700__ $$0241767$$aSchiper, Andre$$g106377
000171619 773__ $$j23$$q341-358$$tDistributed Computing
000171619 8564_ $$s994530$$uhttps://infoscience.epfl.ch/record/171619/files/MC.pdf$$yn/a$$zn/a
000171619 909C0 $$0252206$$pLSR$$xU10411
000171619 909CO $$ooai:infoscience.tind.io:171619$$pIC$$particle$$qGLOBAL_SET
000171619 917Z8 $$x106377
000171619 937__ $$aEPFL-ARTICLE-171619
000171619 973__ $$aEPFL$$rREVIEWED$$sPUBLISHED
000171619 980__ $$aARTICLE