SHF: Small: Computer-Aided Synthesis for Distributed Algorithms

点击翻译按钮获取中文摘要

Formal verification techniques are used to exhaustively test agiven design to detect if it has any possible undesirable behavior.Formal verification is a powerful paradigm since it can detecthard-to-find errors in a design that testing alone is unlikely tofind. However, formal verification techniques can not be used onan incomplete design. This project explores the question of whether such methods be extended to help in the design process by completing a partial design and synthesizing correct systems. Such formal methodscan have a broad impact by influencing the design and correctness of a wide variety of distributed systems.This project develops a general approach for formal model synthesis,called bounded model synthesis, and applies it to do computer-aideddesign of fault-tolerant distributed algorithms. Computation is becoming increasingly distributed, but designing correct, especially fault tolerant, distributed algorithms is an extremely challenging task.The bounded model synthesis approach provides tools that can helpdevelopers perform systematic design of distributed systems.The technical approach consists of lifting verification techniques,such as bounded model checking and k-induction, to perform modelsynthesis. This project develops, implements, and evaluates thebounded model synthesis approach.