2016

SyGuS-Comp 2016: Results and Analysis

Alur, Rajeev, Fisman, Dana, Singh, Rishabh et al.

Understand

Syntax-Guided Synthesis (SyGuS) is the computational problem of finding an implementation f that meets both a semantic constraint given by a logical formula $\varphi$ in a background theory T, and a syntactic constraint given by a grammar G, which specifies the allowed set of candidate implementations.

Such a synthesis problem can be formally defined in SyGuS-IF, a language that is built on top of SMT-LIB.
The Syntax-Guided Synthesis Competition (SyGuS-Comp) is an effort to facilitate, bring together and accelerate research and development of efficient solvers for SyGuS by providing a platform for evaluating different synthesis techniques on a comprehensive set of benchmarks.
In this year's competition we added a new track devoted to programming by examples.

Built on

In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005
Armando Solar-Lezama, Rodric M. Rabbah, Rastislav Bodík & Kemal Ebcioglu (2005): Programming by sketching for bit-streaming programs · 2005
Earlier work this paper cites.
In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia & Vijay A. Saraswat (2006): Combinatorial sketching for finite programs · 2006
Earlier work this paper cites.
In: Proceedings of the 32Nd ACM/IEEE International Conference on Software Engineering - Volume 1
Susmit Jha, Sumit Gulwani, Sanjit A. Seshia & Ashish Tiwari (2010): Oracle-guided Component-based Program Synthesis · 2010
Earlier work this paper cites.
In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010
Saurabh Srivastava, Sumit Gulwani & Jeffrey S. Foster (2010): From program verification to program synthesis · 2010
Earlier work this paper cites.
In: POPL
Sumit Gulwani (2011): Automating string processing in spreadsheets using input-output examples · 2011
Earlier work this paper cites.
Commun. ACM
Sumit Gulwani, William R. Harris & Rishabh Singh (2012): Spreadsheet data manipulation using examples · 2012
Earlier work this paper cites.
In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013
Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2013): Syntax-guided synthesis · 2013
Earlier work this paper cites.
In: OOPSLA
Veselin Raychev, Max Schäfer, Manu Sridharan & Martin T. Vechev (2013): Refactoring with synthesis · 2013
Earlier work this paper cites.
Takuya Akiba, Kentaro Imajo, Hiroaki Iwami, Yoichi Iwata, Toshiki Kataoka, Naohiro Takahashi, Michał Moskal & Nikhil Swamy (2014): Calibrating Research in Program Synthesis Using 72,000 Hours of Programmer Time
2014
Earlier work this paper cites.
In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings
Pranav Garg, Christof Löding, P. Madhusudan & Daniel Neider (2014): ICE: A Robust Framework for Learning Invariants · 2014
Earlier work this paper cites.

Similar

In: Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings
Aaron Stump, Geoff Sutcliffe & Cesare Tinelli (2014): StarExec: A Cross-Community Infrastructure for Logic Solving · 2014
Cited alongside, same era.
In: PLDI
Emina Torlak & Rastislav Bodík (2014): A lightweight symbolic virtual machine for solver-aided host languages · 2014
Cited alongside, same era.
In: Dependable Software Systems Engineering
Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak & Abhishek Udupa (2015): Syntax-Guided Synthesis · 2015
Cited alongside, same era.
In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II
Rajeev Alur, Pavol Cerný & Arjun Radhakrishna (2015): Synthesis Through Unification · 2015
Cited alongside, same era.
In: SYNT
Rajeev Alur, Dana Fisman, Rishabh Singh & Armando Solar-Lezama (2015): Results and Analysis of SyGuS-Comp’15 · 2015
Cited alongside, same era.
In: PLDI
John K. Feser, Swarat Chaudhuri & Isil Dillig (2015): Synthesizing data structure transformations from input-output examples · 2015
Cited alongside, same era.
In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II
Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama & Jeffrey S. Foster (2015): Adaptive Concretization for Parallel Program Synthesis · 2015
Cited alongside, same era.
In: PLDI
Alan Leung, John Sarracino & Sorin Lerner (2015): Interactive parser synthesis by example · 2015
Cited alongside, same era.
In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1
Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang & Daniel Jackson (2015): Alloy*: A General-Purpose Higher-Order Relational Constraint Solver · 2015
Cited alongside, same era.
Private Communication
Daniel Neider, P. Madhusudan & Pranav Garg (2015): ICE DT: Learning Invariants using Decision Trees and Implication Counterexamples · 2015
Cited alongside, same era.
Rajeev Alur, Dana Fisman, P. Madhusudan, Rishabh Singh & Armando Solar-Lezama: SyGuS Syntax for SyGuS-COMP’15
Cited in the paper.
Rajeev Alur, Dana Fisman, Rishabh Singh & Armando Solar-Lezama: SyGuS Syntax for SyGuS-COMP’16
Cited in the paper.

Then

Private Communication
Daniel Neider, Shambwaditya Saha & P. Madhusudan (2015): Alchemist CS: An SMT-based synthesizer for Functions in Linear Integer Arithmetic · 2015
Later among the works it cites.
In: PLDI
Peter-Michael Osera & Steve Zdancewic (2015): Type-and-example-directed program synthesis · 2015
Later among the works it cites.
In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II
Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli & Clark W. Barrett (2015): Counterexample-Guided Quantifier Instantiation for Synthesis in SMT · 2015
Later among the works it cites.
Private Communication
Heinz Riener & Rudiger Ehlers (2015): absTract sOlution Analyzing Synthesis Tool (System Description) · 2015
Later among the works it cites.
In: Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
Shambwaditya Saha, Pranav Garg & P. Madhusudan (2015): Alchemist: Learning Guarded Affine Functions · 2015
Later among the works it cites.
Private Communication
Shambwaditya Saha, Daniel Neider & P. Madhusudan (2015): Alchemist CS DT: Synthesizing Guarded Affine Functions using Constraint Solving and Decision-tree Learning · 2015
Later among the works it cites.
In: 5th Workshop on Synthesis, SYNT 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II
Sarah Chasins & Julie Newcomb (2016): Using SyGuS to Synthesize Reactive Motion Plans · 2016
Closest in time.
In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II
Hassan Eldib, Meng Wu & Chao Wang (2016): Synthesis of Fault-Attack Countermeasures for Cryptographic Circuits · 2016
Closest in time.
In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016
Pranav Garg, Daniel Neider, P. Madhusudan & Dan Roth (2016): Learning invariants using decision trees and implication counterexamples · 2016
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…