The goal of this research theme is to build open-source tools and design environments, and evaluate them for both computational performance and usability. The report in this page focuses on tools that provide an infrastructure to a common theme for a divergence of applications and/or divergence of solvers. We have such infrastructure tools both in the design methodology theme as well as the computational engines theme. Together they may be combined to provide both front-end and back-end engines. In addition we have such infrastructure tool in the theme of challenge problems under robotic systems.
The synthesis tool Sketch Version 1.6, developed by PI Solar-Lezama's group, was recently released. It includes a benchmark suite with a range of synthesis problems that will allow for side-to-side comparisons of synthesis procedures developed by other team members. The Sketch synthesis system is now being used by several of the ExCAPE efforts. PI Foster (Maryland) and his students have been using it to synthesize harnesses for the Android platform as discussed in Section 4.4. PIs Bodik (UC Berkeley) and Seshia (UC Berkeley) have been using it to synthesize reactive controllers. In order to support the use of Sketch by other team members, we have been producing documentation for the language and are in the process of documenting the API so it can be called from within other tools [S13, SSZKS14]. Sketch is being used in the AutoProf system for providing feedback on programming assignments, and the StatusQuo system for improving the performance of database application. Recently, a symbolic SyGuS solver has also been built on top of Sketch using its recursive generators. [See here press article on Sketch]
The Linear Temporal Logic MissiOn Planner (LTLMoP) is an open source, Python-based toolbox developed at Cornell that allows users to control simulated and physical robots by writing high-level specications in structured English and LTL. The toolbox works with the Robot Operating System (ROS) and several robotic platforms such as the iRobot Create and the Aldabaran humanoid Nao. Recently we have added support for the Rice Open Motion Planning Library (OMPL from PI Kavraki's group) and we have integrated it with a natural language processing module [WFK13].
This research explores how to construct synthesizers rapidly, in a prototyping fashion. In particular, we explore how to avoid building a compiler from programs to logical constraints, which is typically the hardest part of the engineering. The crucial observation is that each domain where synthesizers can be useful constitutes a relatively narrow domain, and the synthesis problems thus can be described with a domain-specific language (DSL), eg communicating automata in cache coherence protocols. We showed that these DSLs can be extended with high-level constructs that make the underlying solver conveniently accessible to the programmer. We showed that these solver-aided DSLs can be built easily, by embedding into a host language, in the same fashion as regular languages are embedded into host languages, such as Scala. The embedding of SDSLs is described in [TB14]. In [TB13], we show how to implement the special solveraided host languages. We believe that these results will make it much easier to construct synthesizers.
Solver-aided domain-specific languages (SDSLs) are emerging as a new class of high productivity programming systems. They ease the construction of programs by using SAT and SMT solvers to automate hard programming tasks, such as verification, debugging, synthesis and simulation. But using solvers requires translating programs to logical constraints — a difficult engineering challenge that has limited the availability of SDSLs. We developed a lightweight approach to implementing a solver-aided host language, which frees SDSL designers from having to compile their languages to constraints. New SDSLs are built by standard shallow (library-based) or deep (interpreter-based) embedding into the host language. The host is equipped with a symbolic virtual machine, which compiles only a small subset of the host’s constructs to constraints. The remaining language constructs are stripped away with online partial evaluation. This lightweight compilation is made possible by a novel symbolic execution technique that solves the path explosion problem for a large class of programs. We have used it to implement ROSETTE, a new solver-aided language that is host to several new SDSLs, such as a language for synthesizing web scraping programs.
The library is an open source library that implements sampling-based algorithms and co-safe linear temporal logic specifications. The library allows users to input a robot specification and also a temporal formula in the form of a nondeterministic finite automaton, and choose from a varety of motion planners. The developed synergistic framework allows the satisfaction of the specification while at the same time ensuring a feasible robot motion plan is produced. The library allows for robots with complex dynamics.
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation. The motivation is twofold. First, narrowing the space of implementations makes the synthesis problem more tractable. Second, providing a specific syntax can potentially lead to better optimizations.
In this project we identified the common core of such problems, and formulated it in a logical framework [ABJMRSSLTU]. The input to the syntax-guided synthesis problem consists of a background theory, a semantic correctness specification for the desired program given by a logical formula, and a syntactic set of candidate implementations given by a grammar. The computational problem then is to find an implementation from the set of candidate expressions so that it satisfies the specification in the given theory. This paves the way for building generic solvers for such problems, instead of devising a dedicated algorithm for each such problem anew.
Based on this we initiated a solvers competition SyGuS-COMP (for Syntax-Guided Synthesis Competition) that took place as part of the FLoC Olympic Games, an event of Vienna Summer of Logic 2014. We have made three initial solvers, that can serve as a reference to candidate solvers, publicly available (via StarExec and GitHub): enumerative, symbolic and stochastic.
- R. Alur, R. Bodik, G. Juniwal, M.M.K. Martin, M. Raghothaman, S.A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa. Syntax-guided Synthesis, FMCAD 2013
- R. Singh, R, Singh, Z. Xu, R. Krosnick, A. Solar-Lezama. Modular Synthesis of Sketches Using Models. VMCAI 2014: 395-414
- A. Solar-Lezama. Program sketching. STTT 15(5-6): 475-495 (2013)
- E. Torlak, R. Bodík. A lightweight symbolic virtual machine for solver-aided host languages. PLDI 2014: 54.
- E. Torlak, R. Bodík. Growing solver-aided languages with rosette. Onward! 2013: 135-152
- K. W. Wong, C. Finucane, H. Kress-Gazit. Provably-correct robot control with LTLMoP, OMPL and ROS. IROS 2013: 2073