Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
surveys:synthesis [2010/04/19 16:21] jobstman |
surveys:synthesis [2011/04/19 17:07] (current) jobstman |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Program synthesis ====== | + | ====== Program synthesis (SURVEY UNDER CONSTRUCTION) ====== |
- | In computer science, program synthesis refers to the development of a program or a digital design from a set of desired properties. | + | We use the term **program synthesis** to refer to the development of a program or a digital design from a set of desired properties. |
These properties can be described in various ways, e.g., by a set of logical formulas or a mathematical model, by another program that is | These properties can be described in various ways, e.g., by a set of logical formulas or a mathematical model, by another program that is | ||
- | written in a more abstract programming language. Synthesis is the counterpart to program analysis, which tries to extract a set of properties or a model from a given program or digital design. | + | written in a more abstract programming language. Synthesis is the counterpart to program analysis, which tries to extract a set of properties or a model from a given program or digital design, or program verification, which tries to establish a relationship between a set of properties and the given program or circuit. |
- | The set of desired properties are usually called the //specification of the system// and the constructed system is referred as the | + | The set of desired properties are usually called the **specification of the system** and the constructed system is referred as the |
- | //implementation of the specification.// | + | **implementation of the specification.** |
Line 14: | Line 14: | ||
* Logic synthesis (RTL to gate level, net list to layout,...) | * Logic synthesis (RTL to gate level, net list to layout,...) | ||
* Synthesis from logical specifications | * Synthesis from logical specifications | ||
- | * ... | + | * Model-based design and other domain specific synthesizer: |
+ | * parser generators (YACC) | ||
+ | * generator for statistical analyzers (AutoBayes Synthesis System, Johann M. Schumann, NASA - Moffett Field) | ||
+ | * Matlab Simulink from MathWorks (based on a synchronous dataflow language, generates C/C++ code) | ||
+ | * SCADE Suite from Esterel Technologies (Systems are described using a synchronous language, generates C/C++ code) | ||
+ | * Bluespec compiler (HDL based on rules, each rule is executed automatically, designs have no explicit clock, generates Verilog code) | ||
+ | * BIP compiler (Systems are describe using extended automata and synchronization constructs, generates C/C++ code) | ||
+ | * ... | ||
+ | |||
+ | In the following we will focus on synthesis from logical specifications. | ||
====== Program synthesis from logical specification ====== | ====== Program synthesis from logical specification ====== | ||
Line 20: | Line 29: | ||
**Motivation.** | **Motivation.** | ||
- | A solution to this problem would allow augmenting the current programming style, which is mostly imperative, with a declarative, logical style. This is particularly beneficial for systems in which concurrency plays an important role..... | + | A solution to this problem would allow augmenting the current programming style, which is mostly imperative, with a declarative, logical style. This is particularly beneficial for systems in which concurrency plays an important role. |
In this area approaches can be split into three groups: | In this area approaches can be split into three groups: | ||
Line 97: | Line 106: | ||
source code satisfying the specification. In some cases, the class of generated program is restricted by the set of available statements or an initial incomplete program. | source code satisfying the specification. In some cases, the class of generated program is restricted by the set of available statements or an initial incomplete program. | ||
- | **Approaches.** | + | ====== Approaches ====== |
| **Application** | **Input** | **Output** | **Main Techniques** | **Restrictions** | **Contact person** | | | **Application** | **Input** | **Output** | **Main Techniques** | **Restrictions** | **Contact person** | | ||
Line 107: | Line 116: | ||
| Synchronization mechanism | | | | | E. Yahav| | | Synchronization mechanism | | | | | E. Yahav| | ||
| | | | | | S. Gulwani | | | | | | | | S. Gulwani | | ||
+ | | | | | | | S. Chandra | | ||
| | | | | | V. Kuncak | | | | | | | | V. Kuncak | | ||
| Program Sketching | | | | | R. Bodik | | | Program Sketching | | | | | R. Bodik | | ||
| Deadlock avoidance mechanism | | | | | Y. Wang | | | Deadlock avoidance mechanism | | | | | Y. Wang | | ||
| | | | | | B. Finkbeiner | | | | | | | | B. Finkbeiner | | ||
- | | | | | | | F. Somenzi | | ||
- | | | | | | | Y. Lustig | | ||
- | | | | | | | K. Schneider | | ||
+ | **Dagstuhl Talks** | ||
+ | |Program Sketching | Rastislav Bodik, UC Berkeley | | ||
+ | | | Satish Chandra, IBM TJ Watson Research Center | | ||
+ | | Synthesizing Verifiers for Synthesized Code | Ewen W. Denney, NASA | | ||
+ | | CEGAR for Synthesis | Bernd Finkbeiner, Universität des Saarlandes | | ||
+ | | Dimensions in Program Synthesis | Sumit Gulwani, Microsoft Research | | ||
+ | | Component based Synthesis | Sumit Gulwani, Microsoft Research | | ||
+ | | ? | Shachar Itzhaky, Tel Aviv University | | ||
+ | | Synthesis of Communicating Automata from MSCs | Joost-Pieter Katoen, RWTH Aachen | | ||
+ | | Efficient Synthesis of Asynchronous Systems | Uri Klein, Courant Institute - New York | | ||
+ | | Synthesis Procedures | Viktor Kuncak, EPFL | | ||
+ | | Synthesis as Learning Automata from Examples | Martin Leucker, TU München | | ||
+ | | Systematic Program Design: From Clarity to Efficiency | Yanhong Annie Liu, SUNY - Stony Brook | | ||
+ | | Synthesizing programs using model checking based genetic programming | Doron A. Peled, Bar-Ilan University | | ||
+ | | Synchronous Reactive Synthesis From Linear Temporal Logic Specifications | Nir Piterman, Imperial College London | | ||
+ | | Synthesizing Hardware from Sketches | Andreas Raabe, TU München | | ||
+ | | Software Synthesis is Hard -- and Simple | Sven Schewe, University of Liverpool | | ||
+ | | Data Mining of Air Traffic Track Data for NGATS with the AutoBayes Synthesis System | Johann M. Schumann, NASA | | ||
+ | | Mechanized Algorithm Design | Douglas R. Smith, Kestrel Institute | | ||
+ | | New directions in Computer Supported Programming | Armando Solar-Lezama, MIT | | ||
+ | | Program Synthesis using SMT Solvers | Saurabh Srivastava, University of Maryland | | ||
+ | | Synthesis of Concurrent Algorithms | Martin T. Vechev, IBM TJ Watson Research Center | | ||
+ | | Recursive Plans and Imperative Programs Revisited: Deductive Synthesis | Richard Waldinger, SRI | | ||
+ | | Abstraction-Guided Synthesis of Synchronization | Eran Yahav, IBM TJ Watson Research Center | | ||
+ | | Inferring Synchronization under Limited Observability | Greta Yorsh, IBM TJ Watson Research Center | | ||