Synthesis from formal specifications is a research field with a broad range of methods and applications. Recent years have seen an increased interest in synthesis methods in general, and their practical application in particular. The Workshop on Synthesis aims to bring together researchers working on different aspects of formal synthesis.
Scope and Topics of Interest
The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. It fosters the development of frontier techniques in automating the development of computing systems and is inclusive in its interpretation of the term synthesis:
- Contributions of interest include: algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, benchmark descriptions, and experimental evaluation.
- Computation models include functional, reactive, hybrid and timed systems.
- Application domains include software, hardware, embedded, and cyberphysical systems. Identifying, formalizing, and evaluating synthesis in particular domains is encouraged.
- Of interest are approaches that explore alternative development methods, as well as approaches that improve upon the automation of design, compilation, and optimization techniques currently in widespread use. All appropriate underlying methods are of interest, including above formal methods and techniques that build upon computer-aided verification, but also machine learning and data mining techniques.
- All formalizable forms of specifications of potential practical interest are considered, including contracts, temporal logic specifications, quantitative objectives, partial systems, and (possibly symbolic) input/output examples.
- Of great interest is understanding and productively making use of relationships between synthesis and related topics such as inductive programming, repair, fault localization, testing, discovery (synthesis) of inductive invariants, parameter optimization, constraint solving, theorem proving (including SMT, superposition-based, inductive, and higher-order theorem proving, as well as automated generation of lemmas and knowledge discovery).
- The synthesis workshop hosts two competitions on synthesis tools, the reactive synthesis competition and the syntax-guided synthesis competition. Contributions elaborating on tools and benchmarks submitted to these competitions are encouraged.