Specification decomposition for reactive synthesis.

Reactive synthesis is the task of automatically deriving a correct implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent advances in terms of algorithms and tools, however, reactive synthesis is still not practical when the specified systems reach a certain bound in size and complexity.

Compositional synthesis of modular systems.

In contrast to the breakthroughs in reactive synthesis of monolithic systems, distributed synthesis is not yet practical. Compositional approaches can be a key technique for scalable algorithms. Here, the challenge is to decompose a specification of the global system into local requirements on the individual processes.