Reactive Synthesis with Spectra: A Tutorial

We are proud to host a technical briefing at ICSE'21 to present Spectra developed as part of the SYNTECH project at Tel Aviv University. 

Spectra is a formal specification language specifically tailored for use in the context of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications.

This hands-on tutorial introduces participants to the language and the tool set, using examples and exercises, covering an end-to-end process from specification writing to synthesis to execution. If you want, you can follow the tutorial by starting with installation and setup instructions.

Follow the Spectra tutorial on YouTube in short hands-on sessions

You may find a published overview of the tutorial here. You may cite the tutorial as:

S. Maoz and J. O. Ringert, "Reactive Synthesis with Spectra: A Tutorial," 2021 IEEE/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), 2021, pp. 320-321, doi: 10.1109/ICSE-Companion52605.2021.00136.

A more technical description of the Spectra specification language and some of the analyses provided by Spectra Tools is available. You may cite this article as: 

S. Maoz and J. O. Ringert, "Spectra: a specification language for reactive systems,". Softw Syst Model (2021), doi: 10.1007/s10270-021-00868-z.