TY - GEN
T1 - Abstract learning frameworks for synthesis
AU - Löding, Christof
AU - Madhusudan, P.
AU - Neider, Daniel
N1 - Funding Information:
This work was partially supported by NSF Expeditions in Computing ExCAPE Award #1138994
Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.
Copyright:
Copyright 2016 Elsevier B.V., All rights reserved.
PY - 2016
Y1 - 2016
N2 - We develop abstract learning frameworks for synthesis that embody the principles of the CEGIS (counterexample-guided inductive synthesis) algorithms in current literature. Our framework is based on iterative learning from a hypothesis space that captures synthesized objects, using counterexamples from an abstract sample space, and a concept space that abstractly defines the semantics of synthesis. We show that a variety of synthesis algorithms in current literature can be embedded in this general framework. We also exhibit three general recipes for convergent synthesis: the first two recipes based on finite spaces and Occam learners generalize all techniques of convergence used in existing engines, while the third, involving well-founded quasi-orderings, is new, and we instantiate it to concrete synthesis problems.
AB - We develop abstract learning frameworks for synthesis that embody the principles of the CEGIS (counterexample-guided inductive synthesis) algorithms in current literature. Our framework is based on iterative learning from a hypothesis space that captures synthesized objects, using counterexamples from an abstract sample space, and a concept space that abstractly defines the semantics of synthesis. We show that a variety of synthesis algorithms in current literature can be embedded in this general framework. We also exhibit three general recipes for convergent synthesis: the first two recipes based on finite spaces and Occam learners generalize all techniques of convergence used in existing engines, while the third, involving well-founded quasi-orderings, is new, and we instantiate it to concrete synthesis problems.
UR - http://www.scopus.com/inward/record.url?scp=84964034651&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84964034651&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-49674-9_10
DO - 10.1007/978-3-662-49674-9_10
M3 - Conference contribution
AN - SCOPUS:84964034651
SN - 9783662496732
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 167
EP - 185
BT - Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings
A2 - Raskin, Jean-François
A2 - Chechik, Marsha
PB - Springer-Verlag Berlin Heidelberg
T2 - 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2016 and held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Y2 - 2 April 2016 through 8 April 2016
ER -