(2022) Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
Abstract
While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic modulo theories (TSL-MT), a framework that unites the two approaches to synthesize a single program. In our approach, reactive synthesis and SyGuS collaborate in the synthesis process, and generate executable code that implements both reactive and data-level properties. We present a tool, temos, that combines state-of-the-art methods in reactive synthesis and SyGuS to synthesize programs from TSL-MT specifications. We demonstrate the ap- plicability of our approach over a set of benchmarks, and present a deep case study on synthesizing a music keyboard synthesizer.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | PLDI ACM-SIGPLAN Conference on Programming Language Design and Implementation |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 07 May 2022 15:23 |
| Last Modified: | 09 May 2022 08:29 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3674 |
Actions
Actions (login required)
 |
View Item |