%0 Journal Article %1 tatsuhiro2008using %A Tsuchiya, Tatsuhiro %A Schiper, André %D 2008 %J Distributed Computing %K consensus modelchecking verification %P 466--480 %T Using Bounded Model Checking to Verify Consensus Algorithms %U http://dx.doi.org/10.1007/978-3-540-87779-0_32 %X This paper presents an approach to automatic verification of asynchronous round-based consensus algorithms. We use model checking, a widely practiced verification method; but its application to asynchronous distributed algorithms is difficult because thestate space of these algorithms is often infinite. The proposed approach addresses this difficulty by reducing the verificationproblem to small model checking problems that involve only single phases of algorithm execution. Because a phase consistsof a finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used tosolve these problems. The proposed approach allows us to model check some consensus algorithms up to around 10 processes.

@article{tatsuhiro2008using, abstract = {This paper presents an approach to automatic verification of asynchronous round-based consensus algorithms. We use model checking, a widely practiced verification method; but its application to asynchronous distributed algorithms is difficult because thestate space of these algorithms is often infinite. The proposed approach addresses this difficulty by reducing the verificationproblem to small model checking problems that involve only single phases of algorithm execution. Because a phase consistsof a finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used tosolve these problems. The proposed approach allows us to model check some consensus algorithms up to around 10 processes.}, added-at = {2009-09-16T11:05:00.000+0200}, author = {Tsuchiya, Tatsuhiro and Schiper, André}, biburl = {https://www.bibsonomy.org/bibtex/2c0b972adda976ec1f848d761fa99d7e2/giuliano.losa}, description = {using bounded model checking to verify consensus algorithms}, interhash = {a7a06e0a34fe0f7d756f02cc2a941fca}, intrahash = {c0b972adda976ec1f848d761fa99d7e2}, journal = {Distributed Computing}, keywords = {consensus modelchecking verification}, pages = {466--480}, timestamp = {2009-09-16T11:05:00.000+0200}, title = {Using Bounded Model Checking to Verify Consensus Algorithms}, url = {http://dx.doi.org/10.1007/978-3-540-87779-0_32}, year = 2008 }