Formal verification techniques are used to exhaustively test a given design to detect if it has any possible undesirable behavior. Formal verification is a powerful paradigm since it can detect hard-to-find errors in a design that testing alone is unlikely to find. However, formal verification techniques can not be used on an 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 methods can 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-aided design 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 help developers perform systematic design of distributed systems. The technical approach consists of lifting verification techniques, such as bounded model checking and k-induction, to perform model synthesis. This project develops, implements, and evaluates the bounded model synthesis approach.
