SHF: Small: Computer-Aided Synthesis for Distributed Algorithms

形式化验证技术用于详尽地测试给定的设计，以检测它是否有任何可能的不良行为。形式化验证是一个强大的范例，因为它可以检测到设计中难以发现的错误，而单独测试是不可能发现的。然而，形式化验证技术不能用于不完整的设计。这个项目探讨的问题是，这些方法是否可以通过完成部分设计和合成正确的系统来扩展到设计过程中。这种形式化方法可以通过影响各种分布式系统的设计和正确性而产生广泛的影响。本项目开发了一种正式模型综合的通用方法，称为有界模型综合，并将其应用于容错分布式算法的计算机辅助设计。计算变得越来越分布式，但设计正确的分布式算法，特别是容错算法是一项极具挑战性的任务。有界模型综合方法提供了可以帮助开发人员执行分布式系统系统设计的工具。技术方法包括提升验证技术，如有界模型检查和k-归纳，以执行模型合成。本项目开发、实施和评估有界模型综合方法。

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.