skip to main content

Attention:

The NSF Public Access Repository (NSF-PAR) system and access will be unavailable from 10:00 PM ET on Friday, December 8 until 2:00 AM ET on Saturday, December 9 due to maintenance. We apologize for the inconvenience.

Explore Research Products in the NSF-PAR

Title: Programmable Program Synthesis
Program synthesis is now a reality, and we are approaching the point where domain-specific synthesizers can now handle problems of practical sizes. Moreover, some of these tools are finding adoption in industry. However, for synthesis to become a mainstream technique adopted at large by programmers as well as by end-users, we need to design programmable synthesis frameworks that (i) are not tailored to specific domains or languages, (ii) enable one to specify synthesis problems with a variety of qualitative and quantitative objectives in mind, and (iii) come equipped with theoretical as well as practical guarantees. We report on our work on designing such frameworks and on building synthesis engines that can handle program-synthesis problems describable in such frameworks, and describe open challenges and opportunities.  more » « less
Award ID(s):
1763871
NSF-PAR ID:
10280322
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
Computer Aided Verification
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; ( , Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation)
    null (Ed.)
    Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability. In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms. 
    more » « less
  2. ; ; ; ; ( , The Tenth International Conference on Learning Representations)
    Weak supervision (WS) frameworks are a popular way to bypass hand-labeling large datasets for training data-hungry models. These approaches synthesize multiple noisy but cheaply-acquired estimates of labels into a set of high-quality pseudo-labels for downstream training. However, the synthesis technique is specific to a particular kind of label, such as binary labels or sequences, and each new label type requires manually designing a new synthesis algorithm. Instead, we propose a universal technique that enables weak supervision over any label type while still offering desirable properties, including practical flexibility, computational efficiency, and theoretical guarantees. We apply this technique to important problems previously not tackled by WS frameworks including learning to rank, regression, and learning in hyperbolic space. Theoretically, our synthesis approach produces a consistent estimators for learning some challenging but important generalizations of the exponential family model. Experimentally, we validate our framework and show improvement over baselines in diverse settings including real-world learning-to-rank and regression problems along with learning on hyperbolic manifolds. 
    more » « less
  3. ; ; ( , 2020 IEEE/ACM 28th International Conference on Program Comprehension (ICPC))
    Software traceability provides support for various engineering activities including Program Comprehension; however, it can be challenging and arduous to complete in large industrial projects. Researchers have proposed automated traceability techniques to create, maintain and leverage trace links. Computationally intensive techniques, such as repository mining and deep learning, have showed the capability to deliver accurate trace links. The objective of achieving trusted, automated tracing techniques at industrial scale has not yet been successfully accomplished due to practical performance challenges. This paper evaluates high-performance solutions for deploying effective, computationally expensive traceability algorithms in large scale industrial projects and leverages generated trace links to answer Program Comprehension Queries. We comparatively evaluate four different platforms for supporting industrial-scale tracing solutions, capable of tackling software projects with millions of artifacts. We demonstrate that tracing solutions built using big data frameworks scale well for large projects and that our Spark implementation outperforms relational database, graph database (GraphDB), and plain Java implementations. These findings contradict earlier results which suggested that GraphDB solutions should be adopted for large-scale tracing problems. 
    more » « less
  4. ; ( , ASEE Annual Conference proceedings)
    Practical ingenuity is demonstrated in engineering design through many ways. Students and practitioners alike create many iterations of prototypes in solving problems and design challenges. While focus is on the end product and/or the process employed along the way, this study combines these interests to better understand the product and process through the roles of initial prototyping through the creation of such things as alpha prototypes, conceptual mock-ups, and other rapid prototypes. We explore the purposes and affordances of these low-fidelity prototypes in engineering design activity through both synthesis of different perspectives from literature to compose an integrated framework to characterize prototypes that are developed as part of ideation in designing, as well as historic and student examples and case studies. Studying prototyping (activity) and prototypes (artifacts) is a way to studying design thinking and how students and practitioners learn and apply a problem solving process to their work. Prototyping can make readily evident and explicit (through act of creating and the creations themselves) some of the thinking and insights of the engineering designer into the design problem. Initial, low-fidelity prototypes are characterized as prototypes that are not always elaborate depictions containing all the fine details of the design. In fact, features in a prototype do not always appear in the final design. The underpinning of this work is that prototyping, as a process, is an act of externalizing design thinking, embodying it through physical objects. While several prescriptive frameworks have been developed to describe what prototypes prototype and the role of prototype, the role of low-fidelity prototypes, specifically, lacks sufficient attention. We will present prototyping rather as an holistic mindset that can be a means to approach problem solving in a more accessible manner. It can be helpful to apply this sort of mindset approach from these initial problem understanding through functional decomposition to quickly communicate and learn by trial and building in learning loops to oneself, with an engineering design team, and to potential stakeholders outside the team. 
    more » « less
  5. ; ; ; ; ( , Proceedings of the AAAI Conference on Artificial Intelligence)
    Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning techniques. At its core, the automated reasoning approach relies on highly domain specific knowledge of programming languages. On the other hand, the machine learning approaches utilize the fact that when working with program code, it is possible to generate arbitrarily large training datasets. In this work, we propose a system for using machine learning in tandem with automated reasoning techniques to solve Syntax Guided Synthesis (SyGuS) style PBE problems. By preprocessing SyGuS PBE problems with a neural network, we can use a data driven approach to reduce the size of the search space, then allow automated reasoning-based solvers to more quickly find a solution analytically. Our system is able to run atop existing SyGuS PBE synthesis tools, decreasing the runtime of the winner of the 2019 SyGuS Competition for the PBE Strings track by 47.65% to outperform all of the competing tools. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email