The goal of software synthesis is to generate programs automatically from high-level specifications. However, efficient implementations for challenging programs require a combination of high-level algorithmic insights and low-level implementation details. Deriving the low-level details is a natural job for a computer, but the synthesizer can not replace the human insight. Therefore, one of the central challenges for software synthesis is to establish a synergy between the programmer and the synthesizer, exploiting the programmer's expertise to reduce the burden on the synthesizer.
This thesis introduces sketching , a new style of synthesis that offers a fresh approach to the synergy problem. Previous approaches have relied on meta-programming, or variations of interactive theorem proving to help the synthesizer deduce an efficient implementation. The resulting systems are very powerful, but they require the programmer to master new formalisms far removed from traditional programming models. To make synthesis accessible, programmers must be able to provide their insight effortlessly, using formalisms they already understand.
In Sketching, insight is communicated through a partial program, a sketch that expresses the high-level structure of an implementation but leaves holes in place of the low-level details. This form of synthesis is made possible by a new SAT-based inductive synthesis procedure that can efficiently synthesize an implementation from a small number of test cases. This algorithm forms the core of a new counterexample guided inductive synthesis procedure (CEGIS) which combines the inductive synthesizer with a validation procedure to automatically generate test inputs and ensure that the generated program satisfies its specification. With a few extensions, CEGIS can even use its sequential inductive synthesizer to generate concurrent programs; all the concurrency related reasoning is delegated to an off-the-shelf validation procedure.
The resulting synthesis system scales to real programming problems from a variety of domains ranging from bit-level ciphers to manipulations of linked datastructures. The system was even used to produce a complete optimized implementation of the AES cipher. The concurrency aware synthesizer was also used to synthesize, in a matter of minutes, the details of a fine-locking scheme for a concurrent set, a sense reversing barrier, and even a solution to the dining philosophers problem.
The system was also extended with domain specific knowledge to better handle the problem of implementing stencil computations, an important domain in scientific computing. For this domain, we were able to encode domain specific insight as a problem reduction that converted stencil sketches into simplified sketch problems which CEGIS resolved in a matter of minutes. This specialized synthesizer was used to quickly implement a MultiGrid solver for partial differential equations containing many difficult implementation strategies from the literature.
In short, this thesis shows that sketching is a viable approach to making synthesis practical in a general programming context.
Cited By
- Smith G, Kushigian B, Canumalla V, Cheung A, Lyubomirsky S, Porncharoenwase S, Just R, Bernstein G and Tatlock Z FPGA Technology Mapping Using Sketch-Guided Program Synthesis Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, (416-432)
- Fayolle P and Friedrich M (2024). A Survey of Methods for Converting Unstructured Data to CSG Models, Computer-Aided Design, 168:C, Online publication date: 1-Mar-2024.
- Deng H, Tao R, Peng Y and Wu X (2024). A Case for Synthesis of Recursive Quantum Unitary Programs, Proceedings of the ACM on Programming Languages, 8:POPL, (1759-1788), Online publication date: 5-Jan-2024.
- Liu X, Jang J, Sundaresan N, Allamanis M and Svyatkovskiy A AdaptivePaste: Intelligent Copy-Paste in IDE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (1844-1854)
- Korz N and Andrzejak A Virtual Domain Specific Languages via Embedded Projectional Editing Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, (122-137)
- Yuan Y and Banzhaf W (2023). Iterative genetic improvement, Artificial Intelligence, 322:C, Online publication date: 1-Sep-2023.
- Zheng Q, Xia X, Zou X, Dong Y, Wang S, Xue Y, Shen L, Wang Z, Wang A, Li Y, Su T, Yang Z and Tang J CodeGeeX: A Pre-Trained Model for Code Generation with Multilingual Benchmarking on HumanEval-X Proceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, (5673-5684)
- Khakhar A, Mell S and Bastani O PAC prediction sets for large language models of code Proceedings of the 40th International Conference on Machine Learning, (16237-16249)
- Mell S, Bastani F, Zdancewic S and Bastani O Synthesizing Trajectory Queries from Examples Computer Aided Verification, (459-484)
- Deng Y, Xia C, Peng H, Yang C and Zhang L Large Language Models Are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, (423-435)
- Dong R, Liu J, Zhu Y, Yan C, Mozafari B and Wang X (2023). SlabCity: Whole-Query Optimization Using Program Synthesis, Proceedings of the VLDB Endowment, 16:11, (3151-3164), Online publication date: 1-Jul-2023.
- Barnaby C, Chen Q, Samanta R and Dillig I (2023). ImageEye: Batch Image Processing using Program Synthesis, Proceedings of the ACM on Programming Languages, 7:PLDI, (686-711), Online publication date: 6-Jun-2023.
- Goharshady A, Hitarth S, Mohammadi F and Motwani H (2023). Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs, Proceedings of the ACM on Programming Languages, 7:OOPSLA1, (727-756), Online publication date: 6-Apr-2023.
- Zhang G, Mariano B, Shen X and Dillig I (2023). Automated Translation of Functional Big Data Queries to SQL, Proceedings of the ACM on Programming Languages, 7:OOPSLA1, (580-608), Online publication date: 6-Apr-2023.
- Hu J, Lu E, Holland D, Kawaguchi M, Chong S and Seltzer M (2022). Towards Porting Operating Systems with Program Synthesis, ACM Transactions on Programming Languages and Systems, 45:1, (1-70), Online publication date: 31-Mar-2023.
- Norman C, Godbole A and Manerkar Y PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory Consistency Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, (513-527)
- Daggitt M, Atkey R, Kokke W, Komendantskaya E and Arnaboldi L Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, (102-120)
- Mao J, Lozano-Pérez T, Tenenbaum J and Kaelbling L PDSketch Proceedings of the 36th International Conference on Neural Information Processing Systems, (36972-36984)
- Abate A, Edwards A and Giacobbe M Neural abstractions Proceedings of the 36th International Conference on Neural Information Processing Systems, (26432-26447)
- Cao Y, Li Z, Yang T, Zhang H, Zheng Y, Li Y, Hao J and Liu Y GALOIS Proceedings of the 36th International Conference on Neural Information Processing Systems, (19930-19943)
- Molavi A, Xu A, Diges M, Pick L, Tannu S and Albarghouthi A Qubit Mapping and Routing via MaxSAT Proceedings of the 55th Annual IEEE/ACM International Symposium on Microarchitecture, (1078-1091)
- Aguzzi G, Casadei R and Viroli M Towards Reinforcement Learning-based Aggregate Computing Coordination Models and Languages, (72-91)
- Dong R, Huang Z, Lam I, Chen Y and Wang X WebRobot: web robotic process automation using interactive programming-by-demonstration Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (152-167)
- Schröder M and Cito J Grammars for free Proceedings of the ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results, (41-45)
- Chen Y, Liu J, Feng Y and Bodik R Tree traversal synthesis using domain-specific symbolic compilation Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, (1030-1042)
- Ivanov R, Jothimurugan K, Hsu S, Vaidya S, Alur R and Bastani O (2021). Compositional Learning and Verification of Neural Network Controllers, ACM Transactions on Embedded Computing Systems, 20:5s, (1-26), Online publication date: 31-Oct-2021.
- Heyman G, Huysegems R, Justen P and Van Cutsem T Natural language-guided programming Proceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, (39-55)
- Rahmani K, Raza M, Gulwani S, Le V, Morris D, Radhakrishna A, Soares G and Tiwari A (2021). Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis, Proceedings of the ACM on Programming Languages, 5:OOPSLA, (1-29), Online publication date: 20-Oct-2021.
- Park J, Winterer D, Zhang C and Su Z (2021). Generative type-aware mutation for testing SMT solvers, Proceedings of the ACM on Programming Languages, 5:OOPSLA, (1-19), Online publication date: 20-Oct-2021.
- Nandi C, Willsey M, Zhu A, Wang Y, Saiki B, Anderson A, Schulz A, Grossman D and Tatlock Z (2021). Rewrite rule inference using equality saturation, Proceedings of the ACM on Programming Languages, 5:OOPSLA, (1-28), Online publication date: 20-Oct-2021.
- Park J SMT solver testing with type and grammar based mutation Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (1675-1676)
- Thakkar A, Naik A, Sands N, Alur R, Naik M and Raghothaman M Example-guided synthesis of relational queries Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (1110-1125)
- Shariffdeen R, Noller Y, Grunske L and Roychoudhury A Concolic program repair Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (390-405)
- Park S, Calciu I, Kim T and Kashyap S Contextual concurrency control Proceedings of the Workshop on Hot Topics in Operating Systems, (167-174)
- Presler-Marshall K, Heckman S and Stolee K SQLRepair Proceedings of the 43rd International Conference on Software Engineering: Joint Track on Software Engineering Education and Training, (199-210)
- Mukherjee M, Kant P, Liu Z and Regehr J (2020). Dataflow-based pruning for speeding up superoptimization, Proceedings of the ACM on Programming Languages, 4:OOPSLA, (1-24), Online publication date: 13-Nov-2020.
- Pailoor S, Wang X, Shacham H and Dillig I (2020). Automated policy synthesis for system call sandboxing, Proceedings of the ACM on Programming Languages, 4:OOPSLA, (1-26), Online publication date: 13-Nov-2020.
- Gisi J Synthesizing correct code for machine learning programs Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (1701-1703)
- Fonseca A, Santos P and Silva S The Usability Argument for Refinement Typed Genetic Programming Parallel Problem Solving from Nature – PPSN XVI, (18-32)
- Lubin J, Collins N, Omar C and Chugh R (2020). Program sketching with live bidirectional evaluation, Proceedings of the ACM on Programming Languages, 4:ICFP, (1-29), Online publication date: 2-Aug-2020.
- d'Amorim M, Abreu R and Mello C Visual sketching Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: New Ideas and Emerging Results, (101-104)
- Huang K, Qiu X, Shen P and Wang Y Reconciling enumerative and deductive program synthesis Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, (1159-1174)
- Nandi C, Willsey M, Anderson A, Wilcox J, Darulova E, Grossman D and Tatlock Z Synthesizing structured CAD models with equality saturation and inverse transformations Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, (31-44)
- Winterer D, Zhang C and Su Z Validating SMT solvers via semantic fusion Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, (718-730)
- Samak M, Kim D and Rinard M (2019). Synthesizing replacement classes, Proceedings of the ACM on Programming Languages, 4:POPL, (1-33), Online publication date: 1-Jan-2020.
- Guo Z, James M, Justo D, Zhou J, Wang Z, Jhala R and Polikarpova N (2019). Program synthesis by type-guided abstraction refinement, Proceedings of the ACM on Programming Languages, 4:POPL, (1-28), Online publication date: 1-Jan-2020.
- Hempel B, Lubin J and Chugh R Sketch-n-Sketch Proceedings of the 32nd Annual ACM Symposium on User Interface Software and Technology, (281-292)
- Bavishi R, Lemieux C, Fox R, Sen K and Stoica I (2019). AutoPandas: neural-backed generators for program synthesis, Proceedings of the ACM on Programming Languages, 3:OOPSLA, (1-27), Online publication date: 10-Oct-2019.
- Lou Y, Uddin M, Brown N and Cafarella M Knowledge Graph Programming with a Human-in-the-Loop Proceedings of the Workshop on Human-In-the-Loop Data Analytics, (1-7)
- Illanes L and McIlraith S Generalized planning via abstraction Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, (7610-7618)
- Rosin C Stepping stones to inductive synthesis of low-level looping programs Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, (2362-2370)
- Shi K, Steinhardt J and Liang P (2019). FrAngel: component-based synthesis with control structures, Proceedings of the ACM on Programming Languages, 3:POPL, (1-29), Online publication date: 2-Jan-2019.
- Du T, Inala J, Pu Y, Spielberg A, Schulz A, Rus D, Solar-Lezama A and Matusik W (2018). InverseCSG, ACM Transactions on Graphics, 37:6, (1-16), Online publication date: 31-Dec-2019.
- Feng Y, Martins R, Bastani O and Dillig I (2018). Program synthesis using conflict-driven learning, ACM SIGPLAN Notices, 53:4, (420-435), Online publication date: 2-Dec-2018.
- Wang K, Sullivan A, Marinov D and Khurshid S ASketch: a sketching framework for Alloy Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (916-919)
- Roy S, Pandey A, Dolan-Gavitt B and Hu Y Bug synthesis: challenging bug-finding tools with deep faults Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, (224-234)
- Seshia S and Subramanyan P UCLID5 Proceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design, (1-10)
- Chasins S, Mueller M and Bodik R Rousillon Proceedings of the 31st Annual ACM Symposium on User Interface Software and Technology, (963-975)
- Zhang Z, Wu S, Jiang R, Pan M and Zhang T A Documentation-based Constraint Generation Method for Java APIs Proceedings of the 10th Asia-Pacific Symposium on Internetware, (1-10)
- Nandi C, Wilcox J, Panchekha P, Blau T, Grossman D and Tatlock Z (2018). Functional programming for compiling and decompiling computer-aided design, Proceedings of the ACM on Programming Languages, 2:ICFP, (1-31), Online publication date: 30-Jul-2018.
- Liskowski P, Błądek I and Krawiec K Neuro-guided genetic programming Proceedings of the Genetic and Evolutionary Computation Conference, (1143-1150)
- Feng Y, Martins R, Bastani O and Dillig I Program synthesis using conflict-driven learning Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, (420-435)
- Ahmad M and Cheung A Automatically Leveraging MapReduce Frameworks for Data-Intensive Applications Proceedings of the 2018 International Conference on Management of Data, (1205-1220)
- Loncaric C, Ernst M and Torlak E Generalized data structure synthesis Proceedings of the 40th International Conference on Software Engineering, (958-968)
- Christakopoulou K and Kalai A Glass-box program synthesis Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence and Thirtieth Innovative Applications of Artificial Intelligence Conference and Eighth AAAI Symposium on Educational Advances in Artificial Intelligence, (646-653)
- Wang X, Dillig I and Singh R (2017). Program synthesis using abstraction refinement, Proceedings of the ACM on Programming Languages, 2:POPL, (1-30), Online publication date: 1-Jan-2018.
- Miltner A, Fisher K, Pierce B, Walker D and Zdancewic S (2017). Synthesizing bijective lenses, Proceedings of the ACM on Programming Languages, 2:POPL, (1-30), Online publication date: 1-Jan-2018.
- Wang C, Cheung A and Bodik R (2017). Synthesizing highly expressive SQL queries from input-output examples, ACM SIGPLAN Notices, 52:6, (452-466), Online publication date: 14-Sep-2017.
- Wang C, Cheung A and Bodik R Synthesizing highly expressive SQL queries from input-output examples Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, (452-466)
- Feng Y, Martins R, Wang Y, Dillig I and Reps T (2017). Component-based synthesis for complex APIs, ACM SIGPLAN Notices, 52:1, (599-612), Online publication date: 11-May-2017.
- Jin Z, Anderson M, Cafarella M and Jagadish H Foofah Proceedings of the 2017 ACM International Conference on Management of Data, (683-698)
- Suriana P, Adams A and Kamil S Parallel associative reductions in halide Proceedings of the 2017 International Symposium on Code Generation and Optimization, (281-291)
- Bagheri H, Tang C and Sullivan K (2017). Automated Synthesis and Dynamic Analysis of Tradeoff Spaces for Object-Relational Mapping, IEEE Transactions on Software Engineering, 43:2, (145-163), Online publication date: 1-Feb-2017.
- Feng Y, Martins R, Wang Y, Dillig I and Reps T Component-based synthesis for complex APIs Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (599-612)
- Singh R and Solar-Lezama A Swapper Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, (185-192)
- Ravanbakhsh H and Sankaranarayanan S Robust controller synthesis of switched systems using counterexample guided framework Proceedings of the 13th International Conference on Embedded Software, (1-10)
- Lundquist G, Mohan V and Hamlen K Searching for software diversity Proceedings of the 2016 New Security Paradigms Workshop, (80-91)
- Zhu H, Petri G and Jagannathan S (2016). Automatically learning shape specifications, ACM SIGPLAN Notices, 51:6, (491-507), Online publication date: 1-Aug-2016.
- Loncaric C, Torlak E and Ernst M (2016). Fast synthesis of fast collections, ACM SIGPLAN Notices, 51:6, (355-368), Online publication date: 1-Aug-2016.
- Chugh R, Hempel B, Spradlin M and Albers J (2016). Programmatic and direct manipulation, together at last, ACM SIGPLAN Notices, 51:6, (341-354), Online publication date: 1-Aug-2016.
- Bornholt J, Kaufmann A, Li J, Krishnamurthy A, Torlak E and Wang X (2016). Specifying and Checking File System Crash-Consistency Models, ACM SIGARCH Computer Architecture News, 44:2, (83-98), Online publication date: 29-Jul-2016.
- Farzan A and Kincaid Z Linear arithmetic satisfiability via strategy improvement Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, (735-743)
- Gulwani S Programming by Examples Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706, (9-14)
- Bornholt J, Kaufmann A, Li J, Krishnamurthy A, Torlak E and Wang X (2016). Specifying and Checking File System Crash-Consistency Models, ACM SIGPLAN Notices, 51:4, (83-98), Online publication date: 9-Jun-2016.
- Zhu H, Petri G and Jagannathan S Automatically learning shape specifications Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (491-507)
- Loncaric C, Torlak E and Ernst M Fast synthesis of fast collections Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (355-368)
- Chugh R, Hempel B, Spradlin M and Albers J Programmatic and direct manipulation, together at last Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (341-354)
- Chugh R Prodirect manipulation Proceedings of the 38th International Conference on Software Engineering Companion, (781-784)
- Desai A, Gulwani S, Hingorani V, Jain N, Karkare A, Marron M, R S and Roy S Program synthesis using natural language Proceedings of the 38th International Conference on Software Engineering, (345-356)
- Singh R and Gulwani S (2016). Transforming spreadsheet data types using examples, ACM SIGPLAN Notices, 51:1, (343-356), Online publication date: 8-Apr-2016.
- Bornholt J, Torlak E, Grossman D and Ceze L (2016). Optimizing synthesis with metasketches, ACM SIGPLAN Notices, 51:1, (775-788), Online publication date: 8-Apr-2016.
- Frankle J, Osera P, Walker D and Zdancewic S (2016). Example-directed synthesis: a type-theoretic interpretation, ACM SIGPLAN Notices, 51:1, (802-815), Online publication date: 8-Apr-2016.
- Löding C, Madhusudan P and Neider D Abstract Learning Frameworks for Synthesis Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636, (167-185)
- Bornholt J, Kaufmann A, Li J, Krishnamurthy A, Torlak E and Wang X Specifying and Checking File System Crash-Consistency Models Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, (83-98)
- Gulwani S (2016). Technical Perspective: Program synthesis using stochastic techniques, Communications of the ACM, 59:2, (113-113), Online publication date: 25-Jan-2016.
- Singh R and Gulwani S Transforming spreadsheet data types using examples Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (343-356)
- Bornholt J, Torlak E, Grossman D and Ceze L Optimizing synthesis with metasketches Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (775-788)
- Frankle J, Osera P, Walker D and Zdancewic S Example-directed synthesis: a type-theoretic interpretation Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (802-815)
- Polozov O and Gulwani S (2015). FlashMeta: a framework for inductive program synthesis, ACM SIGPLAN Notices, 50:10, (107-126), Online publication date: 18-Dec-2015.
- Polozov O and Gulwani S FlashMeta: a framework for inductive program synthesis Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, (107-126)
- Gulwani S, Hernández-Orallo J, Kitzelmann E, Muggleton S, Schmid U and Zorn B (2015). Inductive programming meets the real world, Communications of the ACM, 58:11, (90-99), Online publication date: 23-Oct-2015.
- Osera P and Zdancewic S (2015). Type-and-example-directed program synthesis, ACM SIGPLAN Notices, 50:6, (619-630), Online publication date: 7-Aug-2015.
- Srinivasan V and Reps T (2015). Synthesis of machine code from semantics, ACM SIGPLAN Notices, 50:6, (596-607), Online publication date: 7-Aug-2015.
- Zhu L and Kulkarni S Using Model Checking Techniques For Evaluating the Effectiveness of Evolutionary Computing in Synthesis of Distributed Fault-Tolerant Programs Proceedings of the 2015 Annual Conference on Genetic and Evolutionary Computation, (1119-1126)
- Osera P and Zdancewic S Type-and-example-directed program synthesis Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, (619-630)
- Srinivasan V and Reps T Synthesis of machine code from semantics Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, (596-607)
- Delaware B, Pit-Claudel C, Gross J and Chlipala A (2015). Fiat, ACM SIGPLAN Notices, 50:1, (689-700), Online publication date: 11-May-2015.
- Delaware B, Pit-Claudel C, Gross J and Chlipala A Fiat Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (689-700)
- Uhler R and Dave N (2014). Smten with satisfiability-based search, ACM SIGPLAN Notices, 49:10, (157-176), Online publication date: 31-Dec-2015.
- Xu Z, Kamil S and Solar-Lezama A MSL Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, (311-322)
- Uhler R and Dave N Smten with satisfiability-based search Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, (157-176)
- Gulwani S (2014). Example-based learning in computer-aided STEM education, Communications of the ACM, 57:8, (70-80), Online publication date: 1-Aug-2014.
- Singh R, Singh R, Xu Z, Krosnick R and Solar-Lezama A Modular Synthesis of Sketches Using Models Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8318, (395-414)
- Chaudhuri S, Clochard M and Solar-Lezama A (2014). Bridging boolean and quantitative synthesis using smoothed proof search, ACM SIGPLAN Notices, 49:1, (207-220), Online publication date: 13-Jan-2014.
- Chaudhuri S, Clochard M and Solar-Lezama A Bridging boolean and quantitative synthesis using smoothed proof search Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (207-220)
- Solar-Lezama A (2013). Program sketching, International Journal on Software Tools for Technology Transfer (STTT), 15:5-6, (475-495), Online publication date: 1-Oct-2013.
- Singh R, Gulwani S and Solar-Lezama A (2013). Automated feedback generation for introductory programming assignments, ACM SIGPLAN Notices, 48:6, (15-26), Online publication date: 23-Jun-2013.
- Singh R, Gulwani S and Solar-Lezama A Automated feedback generation for introductory programming assignments Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, (15-26)
- Singh R and Solar-Lezama A SPT Proceedings of the 24th international conference on Computer Aided Verification, (738-743)
- Singh R and Solar-Lezama A Synthesizing data structure manipulations from storyboards Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering, (289-299)
- Morgenstern A and Schneider K Program sketching via CTL* model checking Proceedings of the 18th international SPIN conference on Model checking software, (126-143)
- Gulwani S, Korthikanti V and Tiwari A Synthesizing geometry constructions Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, (50-61)
- Gulwani S, Korthikanti V and Tiwari A (2011). Synthesizing geometry constructions, ACM SIGPLAN Notices, 46:6, (50-61), Online publication date: 4-Jun-2011.
- Xu G, Mitchell N, Arnold M, Rountev A and Sevitsky G Software bloat analysis Proceedings of the FSE/SDP workshop on Future of software engineering research, (421-426)
- Gulwani S Dimensions in program synthesis Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, (13-24)
- Hu Z and Gehringer E Improving Feedback on GitHub Pull Requests: A Bots Approach 2019 IEEE Frontiers in Education Conference (FIE), (1-9)
Recommendations
Program sketching
Sketching is a synthesis methodology that aims to bridge the gap between a programmer's high-level insights about a problem and the computer's ability to manage low-level details. In sketching, the programmer uses a partial program, a sketch, to ...
The Sketching Approach to Program Synthesis
APLAS '09: Proceedings of the 7th Asian Symposium on Programming Languages and SystemsSketching is a new form of localized software synthesis that aims to bridge the gap between a programmer's high-level insights about a problem and the computer's ability to manage low-level details. In sketching, the programmer uses partial programs to ...
Algorithmic program synthesis: introduction
Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of ...