Abstract Learning Frameworks for Synthesis
作者： Christof Löding , P. Madhusudan , Daniel Neider
DOI: 10.1007/978-3-662-49674-9_10
关键词: Sample space 、 Semantics (computer science) 、 Convergent synthesis 、 occam 、 Variety (cybernetics) 、 Theoretical computer science 、 Counterexample 、 Space (commercial competition) 、 Artificial intelligence 、 Mathematics 、 Iterative learning control
摘要: We develop abstract learning frameworks for synthesis that embody the principles of CEGIS counterexample-guided inductive algorithms in current literature. Our framework is based on iterative from a hypothesis space captures synthesized objects, using counterexamples an sample space, and concept abstractly defines semantics synthesis. show variety literature can be embedded this general framework. also exhibit three recipes convergent synthesis: first two finite spaces Occam learners generalize all techniques convergence used existing engines, while third, involving well-founded quasi-orderings, new, we instantiate it to concrete problems.
springer.com
core.ac.uk
harvard.edu
arxiv.org
sci-hub.st 参考文章(63)
Tony Hoare, An Axiomatic Basis for Computer Programming Communications of The ACM. ,vol. 12, ,(1969)
Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider, ICE: äAäRobustäFrameworkäforäLearningäInvariants computer aided verification. pp. 69- 87 ,(2014) , 10.1007/978-3-319-08867-9_5
Daniel Neider, Wolfgang Thomas, Martin Leucker, Christof Löding, Applications of automata learning in verification and synthesis Publikationsserver der RWTH Aachen University. ,(2014)
Etienne Kneuss, Manos Koukoutos, Viktor Kuncak, None, Deductive Program Repair computer aided verification. ,vol. 9207, pp. 217- 233 ,(2015) , 10.1007/978-3-319-21668-3_13
Shambwaditya Saha, Pranav Garg, P Madhusudan, None, Alchemist: Learning Guarded Affine Functions Computer Aided Verification. pp. 440- 446 ,(2015) , 10.1007/978-3-319-21690-4_26
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Emanuel Kitzelmann, Inductive Programming: A Survey of Program Synthesis Techniques approaches and applications of inductive programming. pp. 50- 73 ,(2009) , 10.1007/978-3-642-11931-6_3
Cormac Flanagan, K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java formal methods. pp. 500- 517 ,(2001) , 10.1007/3-540-45251-6_29
Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha, Using Language Inference to Verify Omega-Regular Properties Tools and Algorithms for the Construction and Analysis of Systems. ,vol. 3440, pp. 45- 60 ,(2005) , 10.1007/978-3-540-31980-1_4
Steven L. Salzberg, Alberto Segre, Programs for Machine Learning ,(1994)