Linear temporal constraints for sketch-based synthesizers

Sketch-based program synthesis allows users to guide the synthesizer by writing partial programs (sketches). Traditionally, the specifications of these sketches are safety properties expressed either as assertions or semantic equivalences. These specifications, however, lack expressiveness when the user wants to establish how the execution of the desired program evolves over time. This is especially important when synthesizing reactive programs, where the whole specification is about how the computation evolves over time. We explore an alternative method letting the user specify desired program executions as linear temporal logic (LTL) formulae. We define a method for transforming sketches with LTL assertions into sketches with only standard assertions. Specifically, for terminating programs, our method transforms and implements, within the sketch, the LTL formulae as runtime monitors. For non-terminating programs, our procedure defines and implements, into the sketch, fairness conditions (analyzing when an acceptance state of the Büchi automata equivalent to these LTL formulae occurs infinitely often). We prove the correctness of both constructions. Evaluation of our implementation in Sketch shows that our method enables the system to synthesize non-terminating programs, such as a round-robin arbiter for a variable number of devices and a lift controller for a variable number of floors. For terminating programs, our approach improves the synthesizer performance by restricting the search of program candidates without modifying the sketches structures.