Showing 51–60 of 60 results for author: Solar-Lezama, A

Results and Analysis of SyGuS-Comp'15

Authors: Rajeev Alur, Dana Fisman, Rishabh Singh, Armando Solar-Lezama

Abstract: 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… ▽ More 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 two specialized tracks: a track for conditional linear arithmetic, where the grammar need not be specified and is implicitly assumed to be that of the LIA logic of SMT-LIB, and a track for invariant synthesis problems, with special constructs conforming to the structure of an invariant synthesis problem. This paper presents and analyzes the results of SyGuS-comp'15. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: In Proceedings SYNT 2015, arXiv:1602.00786

ACM Class: I.2.2, D.2.4, F.3.1;

Journal ref: EPTCS 202, 2016, pp. 3-26

Program Synthesis from Polymorphic Refinement Types

Authors: Nadia Polikarpova, Ivan Kuraj, Armando Solar-Lezama

Abstract: We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification---and hence synthesis---of nontrivial… ▽ More We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification---and hence synthesis---of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a new algorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input. △ Less

Submitted 21 April, 2016; v1 submitted 28 October, 2015; originally announced October 2015.

ACM Class: F.3.1; I.2.2

Synthesis of Recursive ADT Transformations from Reusable Templates

Authors: Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, Armando Solar-Lezama

Abstract: Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformat… ▽ More Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformations on algebraic data-types. Our approach relies on polymorphic synthesis constructs: a small but powerful extension to the language of syntactic templates, which makes it possible to define a program space in a concise and highly reusable manner, while at the same time retains the scalability benefits of conventional templates. This approach enables end-users to reuse predefined templates from a library for a wide variety of problems with little effort. The paper also describes a novel optimization that further improves the performance and scalability of the system. We evaluated the approach on a set of benchmarks that most notably includes desugaring functions for lambda calculus, which force the synthesizer to discover Church encodings for pairs and boolean operations. △ Less

Submitted 16 April, 2017; v1 submitted 20 July, 2015; originally announced July 2015.

JSKETCH: Sketching for Java

Authors: **seong Jeon, Xiaokang Qiu, Jeffrey S. Foster, Armando Solar-Lezama

Abstract: Sketch-based synthesis, epitomized by the SKETCH tool, lets developers synthesize software starting from a partial program, also called a sketch or template. This paper presents JSKETCH, a tool that brings sketch-based synthesis to Java. JSKETCH's input is a partial Java program that may include holes, which are unknown constants, expression generators, which range over sets of expressions, and cl… ▽ More Sketch-based synthesis, epitomized by the SKETCH tool, lets developers synthesize software starting from a partial program, also called a sketch or template. This paper presents JSKETCH, a tool that brings sketch-based synthesis to Java. JSKETCH's input is a partial Java program that may include holes, which are unknown constants, expression generators, which range over sets of expressions, and class generators, which are partial classes. JSKETCH then translates the synthesis problem into a SKETCH problem; this translation is complex because SKETCH is not object-oriented. Finally, JSKETCH synthesizes an executable Java program by interpreting the output of SKETCH. △ Less

Submitted 13 July, 2015; originally announced July 2015.

Comments: This research was supported in part by NSF CCF-1139021, CCF- 1139056, CCF-1161775, and the partnership between UMIACS and the Laboratory for Telecommunication Sciences

ACM Class: I.2.2; F.3.1

Precise, Dynamic Information Flow for Database-Backed Applications

Authors: Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, Stephen Chong

Abstract: We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic applications. In this paper, we present a programming model that factors out information flow policies… ▽ More We present an approach for dynamic information flow control across the application and database. Our approach reduces the amount of policy code required, yields formal guarantees across the application and database, works with existing relational database implementations, and scales for realistic applications. In this paper, we present a programming model that factors out information flow policies from application code and database queries, a dynamic semantics for the underlying λ^JDB core language, and proofs of termination-insensitive non-interference and policy compliance for the semantics. We implement these ideas in Jacqueline, a Python web framework, and demonstrate feasibility through three application case studies: a course manager, a health record system, and a conference management system used to run an academic workshop. We show that in comparison to traditional applications with hand-coded policy checks, Jacqueline applications have 1) a smaller trusted computing base, 2) fewer lines of policy code, and 2) reasonable, often negligible, additional overheads. △ Less

Submitted 23 April, 2016; v1 submitted 13 July, 2015; originally announced July 2015.

ACM Class: D.3.3

Proceedings Second Workshop on Synthesis

Authors: Bernd Finkbeiner, Armando Solar-Lezama

Abstract: Software synthesis is rapidly develo** into an important research area with vast potential for practical application. The SYNT Workshop on Synthesis aims to bringing together researchers interested in synthesis to present both ongoing and mature work on all aspects of automated synthesis and its applications. The second iteration of SYNT took place in Saint Petersburg, Russia, and was co-loca… ▽ More Software synthesis is rapidly develo** into an important research area with vast potential for practical application. The SYNT Workshop on Synthesis aims to bringing together researchers interested in synthesis to present both ongoing and mature work on all aspects of automated synthesis and its applications. The second iteration of SYNT took place in Saint Petersburg, Russia, and was co-located with the 25th International Conference on Computer Aided Verification. The workshop included eleven presentations covering the full scope of the emerging synthesis community, as well as a discussion lead by Swen Jacobs on the organization of two new synthesis competitions focusing on reactive synthesis and syntax-guided functional synthesis respectively. △ Less

Submitted 27 March, 2014; originally announced March 2014.

Journal ref: EPTCS 142, 2014

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints

Authors: Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, Martin Rinard

Abstract: We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality over string terms (word equations), linear inequality over the length function (length constraints), and membership in regular sets. These questions are important… ▽ More We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality over string terms (word equations), linear inequality over the length function (length constraints), and membership in regular sets. These questions are important in logic, program analysis, and formal verification. Variants of these questions have been studied for many decades by mathematicians. More recently, practical satisfiability procedures (aka SMT solvers) for these formulas have become increasingly important in the context of security analysis for string-manipulating programs such as web applications. We prove three main theorems. First, we give a new proof of undecidability for the validity problem for the set of sentences written as a forall-exists quantifier alternation applied to positive word equations. A corollary of this undecidability result is that this set is undecidable even with sentences with at most two occurrences of a string variable. Second, we consider Boolean combinations of quantifier-free formulas constructed out of word equations and length constraints. We show that if word equations can be converted to a solved form, a form relevant in practice, then the satisfiability problem for Boolean combinations of word equations and length constraints is decidable. Third, we show that the satisfiability problem for quantifier-free formulas over word equations in regular solved form, length constraints, and the membership predicate over regular expressions is also decidable. △ Less

Submitted 25 June, 2013; originally announced June 2013.

Comments: Invited Paper at ADDCT Workshop 2013 (co-located with CADE 2013)

Using Program Synthesis for Social Recommendations

Authors: Alvin Cheung, Armando Solar-Lezama, Samuel Madden

Abstract: This paper presents a new approach to select events of interest to a user in a social media setting where events are generated by the activities of the user's friends through their mobile devices. We argue that given the unique requirements of the social media setting, the problem is best viewed as an inductive learning problem, where the goal is to first generalize from the users' expressed "like… ▽ More This paper presents a new approach to select events of interest to a user in a social media setting where events are generated by the activities of the user's friends through their mobile devices. We argue that given the unique requirements of the social media setting, the problem is best viewed as an inductive learning problem, where the goal is to first generalize from the users' expressed "likes" and "dislikes" of specific events, then to produce a program that can be manipulated by the system and distributed to the collection devices to collect only data of interest. The key contribution of this paper is a new algorithm that combines existing machine learning techniques with new program synthesis technology to learn users' preferences. We show that when compared with the more standard approaches, our new algorithm provides up to order-of-magnitude reductions in model training time, and significantly higher prediction accuracies for our target application. The approach also improves on standard machine learning techniques in that it produces clear programs that can be manipulated to optimize data collection and filtering. △ Less

Submitted 14 August, 2012; originally announced August 2012.

Report number: MIT-CSAIL-TR-2012-025 ACM Class: H.2; I.2.2; H.2.8; D.1.2

Inferring SQL Queries Using Program Synthesis

Authors: Alvin Cheung, Armando Solar-Lezama, Samuel Madden

Abstract: Develo** high-performance applications that interact with databases is a difficult task, as developers need to understand both the details of the language in which their applications are written in, and also the intricacies of the relational model. One popular solution to this problem is the use of object-relational map** (ORM) libraries that provide transparent access to the database using th… ▽ More Develo** high-performance applications that interact with databases is a difficult task, as developers need to understand both the details of the language in which their applications are written in, and also the intricacies of the relational model. One popular solution to this problem is the use of object-relational map** (ORM) libraries that provide transparent access to the database using the same language that the application is written in. Unfortunately, using such frameworks can easily lead to applications with poor performance because developers often end up implementing relational operations in application code, and doing so usually does not take advantage of the optimized implementations of relational operations, efficient query plans, or push down of predicates that database systems provide. In this paper we present QBS, an algorithm that automatically identifies fragments of application logic that can be pushed into SQL queries. The QBS algorithm works by automatically synthesizing invariants and postconditions for the original code fragment. The postconditions and invariants are expressed using a theory of ordered relations that allows us to reason precisely about the contents and order of the records produced even by complex code fragments that compute joins and aggregates. The theory is close in expressiveness to SQL, so the synthesized postconditions can be readily translated to SQL queries. Using 40 code fragments extracted from over 120k lines of open-source code written using the Java Hibernate ORM, we demonstrate that our approach can convert a variety of imperative constructs into relational specifications. △ Less

Submitted 9 August, 2012; originally announced August 2012.

ACM Class: H.2.3; I.2.2; F.3.1

Automated Feedback Generation for Introductory Programming Assignments

Authors: Rishabh Singh, Sumit Gulwani, Armando Solar-Lezama

Abstract: We present a new method for automatically providing feedback for introductory programming problems. In order to use this method, we need a reference implementation of the assignment, and an error model consisting of potential corrections to errors that students might make. Using this information, the system automatically derives minimal corrections to student's incorrect solutions, providing them… ▽ More We present a new method for automatically providing feedback for introductory programming problems. In order to use this method, we need a reference implementation of the assignment, and an error model consisting of potential corrections to errors that students might make. Using this information, the system automatically derives minimal corrections to student's incorrect solutions, providing them with a quantifiable measure of exactly how incorrect a given solution was, as well as feedback about what they did wrong. We introduce a simple language for describing error models in terms of correction rules, and formally define a rule-directed translation strategy that reduces the problem of finding minimal corrections in an incorrect program to the problem of synthesizing a correct program from a sketch. We have evaluated our system on thousands of real student attempts obtained from 6.00 and 6.00x. Our results show that relatively simple error models can correct on average 65% of all incorrect submissions. △ Less

Submitted 16 November, 2012; v1 submitted 8 April, 2012; originally announced April 2012.