Automated Synthesis of Computing Systems

The independent study provides a self-contained introduction to recent advances in automated synthesis of computing systems. We will focus both on classical application of automated synthesis to software engineering and on relatively recent advances in algorithmic synthesis of hardware systems. The course will enable students to be prepared for conducting their own research into automated synthesis of computing systems. This course is taught in Fall semesters. 

Deductive program synthesis (Zohar Manna’s approach), automated synthesis of synchronization in parallel programs (Clarke’s model checking approach), Modern inductive and deductive synthesis of programs, Synthesis of hardware systems with focus on emerging computer architectures and networks, Synthesis applied to customized domains like neural networks and arithmetic circuits.

  1. Manna Z, Waldinger R. A deductive approach to program synthesis. In Readings in artificial intelligence and software engineering 1986 (pp. 3-34). Paper:
  2. Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logic of Programs 1981 May 4 (pp. 52-71). Springer, Berlin, Heidelberg. Paper:
  3. Jha S, Gulwani S, Seshia SA, Tiwari A. Oracle-guided component-based program synthesis. In Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering-Volume 1 2010 May 1 (pp. 215-224). ACM. Paper: Slides are also located here:
  4. Jha S, Seshia SA. A theory of formal synthesis via inductive learning. Acta Informatica. 2017 Nov 1;54(7):693-726. Paper:
  5. Jha S, Raman V, Pinto A, Sahai T, Francis M. On learning sparse boolean formulae for explaining AI decisions. In NASA Formal Methods Symposium 2017 May 16 (pp. 99-114). Springer, Cham. Paper:
  6. Velasquez A, Jha SK. Automated synthesis of crossbars for nanoscale computing using formal methods. In Nanoscale Architectures (NANOARCH), 2015 IEEE/ACM International Symposium on 2015 Jul 8 (pp. 130-136). IEEE. Paper:
  7. Chakraborty D, Jha SK. Automated synthesis of compact crossbars for sneak-path based in-memory computing. In 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE) 2017 Mar 27 (pp. 770-775). IEEE. Paper:
  8. Sun SH, Noh H, Somasundaram S, Lim J. Neural Program Synthesis from Diverse Demonstration Videos. In International Conference on Machine Learning 2018 Jul 3 (pp. 4797-4806). Paper:
  9. Chen H, Wang A, Loo BT. Towards Example-Guided Network Synthesis. In Proceedings of the 2nd Asia-Pacific Workshop on Networking 2018 Aug 2 (pp. 65-71). ACM. Paper:

All papers are freely available from the UCF campus network and the UCF library network. If you have difficulty accessing a paper, please contact the UCF librarian. Evaluation

Performance in this course will be evaluated on the basis of paper reviews(50%), a take-home mid-term (15%) and a take-home final(35%).  Each paper review should summarize the following:

  1. the problem solved by the paper,
  2. the approach taken by the authors, 
  3. an illustration of the approach on a simple example, and
  4. your own thoughts on extending the approach (if any).

Not delivering all of the paper reviews will lead to a failing grade in the class.


Percent of Final Grade



Paper reviews 











Grading Scale (%)




80 - 89


70 - 79


60 - 69


50 - 59


40 - 50


0 - 40











fall2018_cot_6908-0003_automated_synthesis_of_computing_systems_.pdf69 KB
fall2018_contract_cot_6908-0003_automated_synthesis_of_computing_systems_.pdf675 KB