Synthesizing Reactive Programs

Author Parthasarathy Madhusudan

Thumbnail PDF


  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

Parthasarathy Madhusudan

Cite AsGet BibTex

Parthasarathy Madhusudan. Synthesizing Reactive Programs. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 428-442, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


Current theoretical solutions to the classical Church's synthesis problem are focused on synthesizing transition systems and not programs. Programs are compact and often the true aim in many synthesis problems, while the transition systems that correspond to them are often large and not very useful as synthesized artefacts. Consequently, current practical techniques first synthesize a transition system, and then extract a more compact representation from it. We reformulate the synthesis of reactive systems directly in terms of program synthesis, and develop a theory to show that the problem of synthesizing programs over a fixed set of Boolean variables in a simple imperative programming language is decidable for regular omega-specifications. We also present results for synthesizing programs with recursion against both regular specifications as well as visibly-pushdown language specifications. Finally, we show applications to program repair, and conclude with open problems in synthesizing distributed programs.
  • program synthesis
  • boolean programs
  • automata theory
  • temporal logics


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail