Parameterized Synthesis of Concurrent and Distributed System

Program synthesis is one of the branches of the field of formal methods. The goal of synthesis methods is to automatically construct systems from a formal specification, relieving the designer from tedious and error-prone manual implementation of the system. In concurrent and distributed systems, the interplay between separate components makes it notoriously hard to construct correct systems manually, resulting in a large potential benefit of synthesis methods. Despite this, there has only been little research in this area. We propose to develop new methods for the synthesis of concurrent and distributed systems that are parameterized in the number of components. The goal is to enhance our understanding of the synthesis problem for such systems, as well as developing synthesis tools and facilitating their integration into the design process of parameterized systems. To this end, we will combine insights from research on verification and synthesis methods for different classes of distributed systems. We propose the following specific research directions: (1)developing efficient synthesis procedures that produce correct-by-construction distributed systems with a fixed number of components, by generalizing and optimizing existing methods for verification and synthesis; (2)extending the applicability of our existing approach for parameterized synthesis that uses decidability results from parameterized verification to reduce the parameterized synthesis problem to a synthesis problem with a fixed number of components; methods from (1) can then be used to solve the resulting problem; (3)designing synthesis approaches that interleave abstraction-based parameterized verification techniques (for systems with undecidable verification problem) with synthesis approaches that are guided by failed verification attempts; these will use the methods from (1) as subprocedures; (4)proving feasibility by applying the resulting methods to challenging benchmark case studies, in particular the synthesis of cache coherence protocols.