Synthesis is the task of automatically deriving correct-by-construction implementations from formal specifications. While it is a promising path toward developing verified programs, it is infamous for being hard to solve. Compositionality is recognized as a key technique for reducing the complexity of synthesis. So far, compositional approaches require extensive manual effort. In this thesis, we introduce algorithms that automate these steps.

In the first part, we develop compositional synthesis techniques for distributed systems. Providing assumptions on other processes’ behavior is fundamental in this setting due to inter- process dependencies. We establish delay-dominance, a new requirement for implementations that allows for implicitly assuming that other processes will not maliciously violate the shared goal. Furthermore, we present an algorithm that computes explicit assumptions on process behavior to address more complex dependencies.

In the second part, we transfer the concept of compositionality from distributed to single- process systems. We present a preprocessing technique for synthesis that identifies indepen- dently synthesizable system components. We extend this approach to an incremental synthesis algorithm, resulting in more fine-grained decompositions. Our experimental evaluation shows that our techniques automate the required manual efforts, resulting in fully automated compo- sitional synthesis algorithms for both distributed and single-process systems.