[4F3-OS-8b] AIと制約プログラミング(2/2)

[4F3-OS-8b-01] Verification and testing of distributed algorithms with a SAT solver

〇Tatsuhiro Tsuchiya¹ (1. Osaka University)

Keywords:satisfiability, bounded model checking, distributed algorithms

Distributed algorithms are difficult to design correctly because they need to cope with a myriad of scenarios caused by concurrency and communication and process failures. This article presents a simple method to detect bugs in distributed algorithms by using SAT-based techniques such as bounded model checking. The results of applying the proposed method to a few examples are shown.