Reactive programs are those that process external events, such as signals and messages. Device drivers and cloud microservices are examples of reactive programs. A system built from reactive programs is concurrent and exhibits a high degree of nondeterminism, making non-exhaustive testing inadequate. Specification languages simplify the design and verification of algorithms, but specification proofs say nothing about implementations.

Program synthesis is one way to bridge this disconnect. A synthesizer searches a space of candidate programs for an implementation that satisfies the specification. Unfortunately, synthesis of non-trivial programs becomes intractable as the search space grows exponentially. Recent work in symbolic execution and solver-aided synthesis has advanced the state of the art, but symbolic techniques also lead to exponential blowup.

COMET is a system for synthesizing reactive programs from unbounded nondeterministic iterative transformations (UNITY) specifications. Naïve synthesis using symbolic execution scales poorly due to the complex values generated by layers of symbolic execution. COMET reduces the complexity of symbolic values, enabling task decomposition. COMET synthesizes non-trivial programs for sequential and concurrent languages by applying three techniques: symbolic execution of the specification into guarded traces, intermediate target trace synthesis, and recursive synthesis of target expressions. We demonstrate this approach by synthesizing Arduino and Verilog implementations from UNITY specifications of the Paxos consensus proposer and acceptor roles. COMET synthesizes the acceptor and proposer in 11 and 45 minutes respectively.