https://en.wikipedia.org/wiki/Program_synthesis

Jump to content
[ ] Main menu
Main menu
move to sidebar hide
Navigation

  * Main page
  * Contents
  * Current events
  * Random article
  * About Wikipedia
  * Contact us
  * Donate

Contribute

  * Help
  * Learn to edit
  * Community portal
  * Recent changes
  * Upload file

[wikipe] Wikipedia The Free Encyclopedia
Search
[                    ]
Search

  * Create account
  * Log in

[ ] Personal tools

  * Create account
  * Log in

Pages for logged out editors learn more

  * Contributions
  * Talk

Contents

move to sidebar hide

  *  
    (Top)
  *  
    1Origin
  *  
    221st century developments
    Toggle 21st century developments subsection
      +  
        2.1Syntax-guided synthesis
  *  
    3The framework of Manna and Waldinger
    Toggle The framework of Manna and Waldinger subsection
      +  
        3.1Proof rules
      +  
        3.2Example
  *  
    4See also
  *  
    5Notes
  *  
    6References

[ ] Toggle the table of contents

Program synthesis

[ ] 4 languages

  * l`rby@
  * Francais
  * hangugeo
  * Ri Ben Yu 

Edit links

  * Article
  * Talk

[ ] English

  * Read
  * Edit
  * View history

[ ] Tools
Tools
move to sidebar hide
Actions

  * Read
  * Edit
  * View history

General

  * What links here
  * Related changes
  * Upload file
  * Special pages
  * Permanent link
  * Page information
  * Cite this page
  * Get shortened URL
  * Download QR code
  * Wikidata item

Print/export

  * Download as PDF
  * Printable version

From Wikipedia, the free encyclopedia

In computer science, program synthesis is the task to construct a
program that provably satisfies a given high-level formal
specification. In contrast to program verification, the program is to
be constructed rather than given; however, both fields make use of
formal proof techniques, and both comprise approaches of different
degrees of automation. In contrast to automatic programming
techniques, specifications in program synthesis are usually non-
algorithmic statements in an appropriate logical calculus.^[1]

The primary application of program synthesis is to relieve the
programmer of the burden of writing correct, efficient code that
satisfies a specification. However, program synthesis also has
applications to superoptimization and inference of loop invariants.^
[2]

Origin[edit]

During the Summer Institute of Symbolic Logic at Cornell University
in 1957, Alonzo Church defined the problem to synthesize a circuit
from mathematical requirements.^[3] Even though the work only refers
to circuits and not programs, the work is considered to be one of the
earliest descriptions of program synthesis and some researchers refer
to program synthesis as "Church's Problem". In the 1960s, a similar
idea for an "automatic programmer" was explored by researchers in
artificial intelligence.^[citation needed]

Since then, various research communities considered the problem of
program synthesis. Notable works include the 1969 automata-theoretic
approach by Buchi and Landweber,^[4] and the works by Manna and
Waldinger (c. 1980). The development of modern high-level programming
languages can also be understood as a form of program synthesis.

21st century developments[edit]

       This section needs expansion with: a more detailed overview of
[icon] contemporary approaches. You can help by adding to it. (
       December 2022)

The early 21st century has seen a surge of practical interest in the
idea of program synthesis in the formal verification community and
related fields. Armando Solar-Lezama showed that it is possible to
encode program synthesis problems in Boolean logic and use algorithms
for the Boolean satisfiability problem to automatically find
programs.^[5]

Syntax-guided synthesis[edit]

In 2013, a unified framework for program synthesis problems called
Syntax-guided Synthesis (stylized SyGuS) was proposed by researchers
at UPenn, UC Berkeley, and MIT.^[6] The input to a SyGuS algorithm
consists of a logical specification along with a context-free grammar
of expressions that constrains the syntax of valid solutions.^[7] For
example, to synthesize a function f that returns the maximum of two
integers, the logical specification might look like this:

(f(x,y) = x [?] f(x,y) = y) [?] f(x,y) >= x [?] f(x,y) >= y

and the grammar might be:

<Exp> ::= x | y | 0 | 1 | <Exp> + <Exp> | ite(<Cond>, <Exp>, <Exp>)
<Cond> ::= <Exp> <= <Exp>

where "ite" stands for "if-then-else". The expression

ite(x <= y, y, x)

would be a valid solution, because it conforms to the grammar and the
specification.

From 2014 through 2019, the yearly Syntax-Guided Synthesis
Competition (or SyGuS-Comp) compared the different algorithms for
program synthesis in a competitive event.^[8] The competition used a
standardized input format, SyGuS-IF, based on SMT-Lib 2. For example,
the following SyGuS-IF encodes the problem of synthesizing the
maximum of two integers (as presented above):

(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
  ((i Int) (c Int) (b Bool))
  ((i Int (c x y (+ i i) (ite b i i)))
   (c Int (0 1))
   (b Bool ((<= i i)))))
(declare-var x Int)
(declare-var y Int)
(constraint (>= (f x y) x))
(constraint (>= (f x y) y))
(constraint (or (= (f x y) x) (= (f x y) y)))
(check-synth)

A compliant solver might return the following output:

((define-fun f ((x Int) (y Int)) Int (ite (<= x y) y x)))

The framework of Manna and Waldinger[edit]

   Non-clausal resolution rules (unifying substitutions not shown)
Nr        Assertions                  Goals           Program Origin
   E [ p ] {\displaystyle E
51 [p]} {\displaystyle E
   [p]}
   F [ p ] {\displaystyle F
52 [p]} {\displaystyle F
   [p]}
53                          G [ p ] {\displaystyle G  s
                            [p]} {\displaystyle G[p]}
54                          H [ p ] {\displaystyle H  t
                            [p]} {\displaystyle H[p]}
   E [ true ] [?] F [ false ]
   {\displaystyle E[{\text
   {true}}]\lor F[{\text                                      Resolve
55 {false}}]} {\                                              (51,52)
   displaystyle E[{\text
   {true}}]\lor F[{\text
   {false}}]}
                            ! F [ true ] [?] G [ false
                            ] {\displaystyle \lnot F
                            [{\text{true}}]\land G[{\         Resolve
56                          text{false}}]} {\         s       (52,53)
                            displaystyle \lnot F[{\
                            text{true}}]\land G[{\
                            text{false}}]}
                            ! F [ false ] [?] G [ true
                            ] {\displaystyle \lnot F
                            [{\text{false}}]\land G           Resolve
57                          [{\text{true}}]} {\       s       (53,52)
                            displaystyle \lnot F[{\
                            text{false}}]\land G[{\
                            text{true}}]}
                            G [ true ] [?] H [ false ]
                            {\displaystyle G[{\text
58                          {true}}]\land H[{\text    p ? s : Resolve
                            {false}}]} {\displaystyle t       (53,54)
                            G[{\text{true}}]\land H
                            [{\text{false}}]}

The framework of Manna and Waldinger, published in 1980,^[9]^[10]
starts from a user-given first-order specification formula. For that
formula, a proof is constructed, thereby also synthesizing a
functional program from unifying substitutions.

The framework is presented in a table layout, the columns containing:

  * A line number ("Nr") for reference purposes
  * Formulas that already have been established, including axioms and
    preconditions, ("Assertions")
  * Formulas still to be proven, including postconditions, ("Goals"),
    ^[note 1]
  * Terms denoting a valid output value ("Program")^[note 2]
  * A justification for the current line ("Origin")

Initially, background knowledge, pre-conditions, and post-conditions
are entered into the table. After that, appropriate proof rules are
applied manually. The framework has been designed to enhance human
readability of intermediate formulas: contrary to classical
resolution, it does not require clausal normal form, but allows one
to reason with formulas of arbitrary structure and containing any
junctors ("non-clausal resolution"). The proof is complete when t r u
e {\displaystyle {\it {true}}} {\displaystyle {\it {true}}} has been
derived in the Goals column, or, equivalently, f a l s e {\
displaystyle {\it {false}}} {\displaystyle {\it {false}}} in the
Assertions column. Programs obtained by this approach are guaranteed
to satisfy the specification formula started from; in this sense they
are correct by construction.^[11] Only a minimalist, yet
Turing-complete,^[12] purely functional programming language,
consisting of conditional, recursion, and arithmetic and other
operators^[note 3] is supported. Case studies performed within this
framework synthesized algorithms to compute e.g. division, remainder,
^[13] square root,^[14] term unification,^[15] answers to relational
database queries^[16] and several sorting algorithms.^[17]^[18]

Proof rules[edit]

Proof rules include:

  * Non-clausal resolution (see table).

    For example, line 55 is obtained by resolving Assertion formulas 
    E {\displaystyle E} {\displaystyle E} from 51 and F {\
    displaystyle F} {\displaystyle F} from 52 which both share some
    common subformula p {\displaystyle p} {\displaystyle p}. The
    resolvent is formed as the disjunction of E {\displaystyle E} {\
    displaystyle E}, with p {\displaystyle p} {\displaystyle p}
    replaced by t r u e {\displaystyle {\it {true}}} {\displaystyle
    {\it {true}}}, and F {\displaystyle F} {\displaystyle F}, with p
    {\displaystyle p} {\displaystyle p} replaced by f a l s e {\
    displaystyle {\it {false}}} {\displaystyle {\it {false}}}. This
    resolvent logically follows from the conjunction of E {\
    displaystyle E} {\displaystyle E} and F {\displaystyle F} {\
    displaystyle F}. More generally, E {\displaystyle E} {\
    displaystyle E} and F {\displaystyle F} {\displaystyle F} need to
    have only two unifiable subformulas p 1 {\displaystyle p_{1}} {\
    displaystyle p_{1}} and p 2 {\displaystyle p_{2}} {\displaystyle
    p_{2}}, respectively; their resolvent is then formed from E th {\
    displaystyle E\theta } {\displaystyle E\theta } and F th {\
    displaystyle F\theta } {\displaystyle F\theta } as before, where 
    th {\displaystyle \theta } {\displaystyle \theta } is the most
    general unifier of p 1 {\displaystyle p_{1}} {\displaystyle p_
    {1}} and p 2 {\displaystyle p_{2}} {\displaystyle p_{2}}. This
    rule generalizes resolution of clauses.^[19]
    Program terms of parent formulas are combined as shown in line 58
    to form the output of the resolvent. In the general case, th {\
    displaystyle \theta } {\displaystyle \theta } is applied to the
    latter also. Since the subformula p {\displaystyle p} {\
    displaystyle p} appears in the output, care must be taken to
    resolve only on subformulas corresponding to computable
    properties.

  * Logical transformations.

    For example, E [?] ( F [?] G ) {\displaystyle E\land (F\lor G)} {\
    displaystyle E\land (F\lor G)} can be transformed to ( E [?] F ) [?]
    ( E [?] G ) {\displaystyle (E\land F)\lor (E\land G)} {\
    displaystyle (E\land F)\lor (E\land G)}) in Assertions as well as
    in Goals, since both are equivalent.

  * Splitting of conjunctive assertions and of disjunctive goals.

    An example is shown in lines 11 to 13 of the toy example below.

  * Structural induction.

    This rule allows for synthesis of recursive functions. For a
    given pre- and postcondition "Given x {\displaystyle x} {\
    displaystyle x} such that pre ( x ) {\displaystyle {\textit
    {pre}}(x)} {\displaystyle {\textit {pre}}(x)}, find f ( x ) = y
    {\displaystyle f(x)=y} {\displaystyle f(x)=y} such that post ( x
    , y ) {\displaystyle {\textit {post}}(x,y)} {\displaystyle {\
    textit {post}}(x,y)}", and an appropriate user-given
    well-ordering [?] {\displaystyle \prec } {\displaystyle \prec } of
    the domain of x {\displaystyle x} {\displaystyle x}, it is always
    sound to add an Assertion " x ' [?] x [?] pre ( x ' ) [?] post ( x ' ,
    f ( x ' ) ) {\displaystyle x'\prec x\land {\textit {pre}}(x')\
    implies {\textit {post}}(x',f(x'))} {\displaystyle x'\prec x\land
    {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}".^[20]
    Resolving with this assertion can introduce a recursive call to f
    {\displaystyle f} {\displaystyle f} in the Program term.
    An example is given in Manna, Waldinger (1980), p.108-111, where
    an algorithm to compute quotient and remainder of two given
    integers is synthesized, using the well-order ( n ' , d ' ) [?] ( n
    , d ) {\displaystyle (n',d')\prec (n,d)} {\displaystyle (n',d')\
    prec (n,d)} defined by 0 <= n ' < n {\displaystyle 0\leq n'<n} {\
    displaystyle 0\leq n'<n} (p.110).

Murray has shown these rules to be complete for first-order logic.^
[21] In 1986, Manna and Waldinger added generalized E-resolution and
paramodulation rules to handle also equality;^[22] later, these rules
turned out to be incomplete (but nevertheless sound).^[23]

Example[edit]

                Example synthesis of maximum function
Nr    Assertions               Goals            Program    Origin
   A = A {\
   displaystyle A=
1  A} {\                                                Axiom
   displaystyle A=
   A}
   A <= A {\
   displaystyle A\
2  leq A} {\                                            Axiom
   displaystyle A\
   leq A}
   A <= B [?] B <= A {\
   displaystyle A\
   leq B\lor B\leq
3  A} {\                                                Axiom
   displaystyle A\
   leq B\lor B\leq
   A}
                    x <= M [?] y <= M [?] ( x = M [?] y
                    = M ) {\displaystyle x\leq
10                  M\land y\leq M\land (x=M\   M       Specification
                    lor y=M)} {\displaystyle x\
                    leq M\land y\leq M\land (x=
                    M\lor y=M)}
                    ( x <= M [?] y <= M [?] x = M ) [?]
                    ( x <= M [?] y <= M [?] y = M )
                    {\displaystyle (x\leq M\
                    land y\leq M\land x=M)\lor
11                  (x\leq M\land y\leq M\land  M       Distr(10)
                    y=M)} {\displaystyle (x\leq
                    M\land y\leq M\land x=M)\
                    lor (x\leq M\land y\leq M\
                    land y=M)}
                    x <= M [?] y <= M [?] x = M {\
                    displaystyle x\leq M\land y
12                  \leq M\land x=M} {\         M       Split(11)
                    displaystyle x\leq M\land y
                    \leq M\land x=M}
                    x <= M [?] y <= M [?] y = M {\
                    displaystyle x\leq M\land y
13                  \leq M\land y=M} {\         M       Split(11)
                    displaystyle x\leq M\land y
                    \leq M\land y=M}
                    x <= x [?] y <= x {\
14                  displaystyle x\leq x\land y x       Resolve(12,1)
                    \leq x} {\displaystyle x\
                    leq x\land y\leq x}
15                  y <= x {\displaystyle y\leq  x       Resolve(14,2)
                    x} {\displaystyle y\leq x}
                    ! ( x <= y ) {\displaystyle
16                  \lnot (x\leq y)} {\         x       Resolve(15,3)
                    displaystyle \lnot (x\leq
                    y)}
                    x <= y [?] y <= y {\
17                  displaystyle x\leq y\land y y       Resolve(13,1)
                    \leq y} {\displaystyle x\
                    leq y\land y\leq y}
18                  x <= y {\displaystyle x\leq  y       Resolve(17,2)
                    y} {\displaystyle x\leq y}
                    true {\displaystyle {\
19                  textit {true}}} {\          x<y ? y Resolve
                    displaystyle {\textit       : x     (18,16)
                    {true}}}

As a toy example, a functional program to compute the maximum M {\
displaystyle M} {\displaystyle M} of two numbers x {\displaystyle x} 
{\displaystyle x} and y {\displaystyle y} {\displaystyle y} can be
derived as follows.^[citation needed]

Starting from the requirement description "The maximum is larger than
or equal to any given number, and is one of the given numbers", the
first-order formula [?] X [?] Y [?] M : X <= M [?] Y <= M [?] ( X = M [?] Y = M )
{\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land
(X=M\lor Y=M)} {\displaystyle \forall X\forall Y\exists M:X\leq M\
land Y\leq M\land (X=M\lor Y=M)} is obtained as its formal
translation. This formula is to be proved. By reverse Skolemization,^
[note 4] the specification in line 10 is obtained, an upper- and
lower-case letter denoting a variable and a Skolem constant,
respectively.

After applying a transformation rule for the distributive law in line
11, the proof goal is a disjunction, and hence can be split into two
cases, viz. lines 12 and 13.

Turning to the first case, resolving line 12 with the axiom in line 1
leads to instantiation of the program variable M {\displaystyle M} {\
displaystyle M} in line 14. Intuitively, the last conjunct of line 12
prescribes the value that M {\displaystyle M} {\displaystyle M} must
take in this case. Formally, the non-clausal resolution rule shown in
line 57 above is applied to lines 12 and 1, with

  * p being the common instance x=x of A=A and x=M, obtained by
    syntactically unifying the latter formulas,
  * F[p] being true [?] x=x, obtained from instantiated line 1
    (appropriately padded to make the context F[[?]] around p visible),
    and
  * G[p] being x <= x [?] y <= x [?] x = x, obtained from instantiated line
    12,

yielding ! ( {\displaystyle \lnot (} {\displaystyle \lnot (}true [?] 
false) [?] (x <= x [?] y <= x [?] true ) {\displaystyle )} {\displaystyle )},
which simplifies to x <= x [?] y <= x {\displaystyle x\leq x\land y\leq
x} {\displaystyle x\leq x\land y\leq x}.

In a similar way, line 14 yields line 15 and then line 16 by
resolution. Also, the second case, x <= M [?] y <= M [?] y = M {\
displaystyle x\leq M\land y\leq M\land y=M} {\displaystyle x\leq M\
land y\leq M\land y=M} in line 13, is handled similarly, yielding
eventually line 18.

In a last step, both cases (i.e. lines 16 and 18) are joined, using
the resolution rule from line 58; to make that rule applicable, the
preparatory step 15-16 was needed. Intuitively, line 18 could be read
as "in case x <= y {\displaystyle x\leq y} {\displaystyle x\leq y},
the output y {\displaystyle y} {\displaystyle y} is valid (with
respect to the original specification), while line 15 says "in case y
<= x {\displaystyle y\leq x} {\displaystyle y\leq x}, the output x {\
displaystyle x} {\displaystyle x} is valid; the step 15-16
established that both cases 16 and 18 are complementary.^[note 5]
Since both line 16 and 18 comes with a program term, a conditional
expression results in the program column. Since the goal formula true
{\displaystyle {\textit {true}}} {\displaystyle {\textit {true}}} has
been derived, the proof is done, and the program column of the " true
{\displaystyle {\textit {true}}} {\displaystyle {\textit {true}}}"
line contains the program.

See also[edit]

  * Inductive programming
  * Metaprogramming
  * Program derivation
  * Natural language programming
  * Reactive synthesis

Notes[edit]

 1. ^ The distinction "Assertions" / "Goals" is for convenience only;
    following the paradigm of proof by contradiction, a Goal F {\
    displaystyle F} {\displaystyle F} is equivalent to an assertion !
    F {\displaystyle \lnot F} {\displaystyle \lnot F}.
 2. ^ When F {\displaystyle F} {\displaystyle F} and s {\displaystyle
    s} {\displaystyle s} is the Goal formula and the Program term in
    a line, respectively, then in all cases where F {\displaystyle F}
    {\displaystyle F} holds, s {\displaystyle s} {\displaystyle s} is
    a valid output of the program to be synthesized. This invariant
    is maintained by all proof rules. An Assertion formula usually is
    not associated with a Program term.
 3. ^ Only the conditional operator (?:) is supported from the
    beginning. However, arbitrary new operators and relations can be
    added by providing their properties as axioms. In the toy example
    below, only the properties of = {\displaystyle =} {\displaystyle
    =} and <= {\displaystyle \leq } {\displaystyle \leq } that are
    actually needed in the proof have been axiomatized, in line 1 to
    3.
 4. ^ While ordinary Skolemization preserves satisfiability, reverse
    Skolemization, i.e. replacing universally quantified variables by
    functions, preserves validity.
 5. ^ Axiom 3 was needed for that; in fact, if <= {\displaystyle \leq
    } {\displaystyle \leq } wasn't a total order, no maximum could be
    computed for uncomparable inputs x , y {\displaystyle x,y} {\
    displaystyle x,y}.

References[edit]

 1. ^ Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer
    Nilsson, J. (2004). "Synthesis of programs in computational
    logic". In M. Bruynooghe and K.-K. Lau (ed.). Program Development
    in Computational Logic. LNCS. Vol. 3049. Springer. pp. 30-65.
    CiteSeerX 10.1.1.62.4976.
 2. ^ (Alur, Singh & Fisman) harv error: no target:
    CITEREFAlurSinghFisman (help)
 3. ^ Alonzo Church (1957). "Applications of recursive arithmetic to
    the problem of circuit synthesis". Summaries of the Summer
    Institute of Symbolic Logic. 1: 3-50.
 4. ^ Richard Buchi, Lawrence Landweber (Apr 1969). "Solving
    Sequential Conditions by Finite-State Strategies". Transactions
    of the American Mathematical Society. 138: 295-311. doi:10.2307/
    1994916. JSTOR 1994916.
 5. ^ Solar-Lezama, Armando (2008). Program synthesis by sketching 
    (PDF) (Ph.D.). University of California, Berkeley.
 6. ^ Alur, Rajeev; al., et (2013). "Syntax-guided Synthesis".
    Proceedings of Formal Methods in Computer-Aided Design. IEEE.
    p. 8.
 7. ^ David, Cristina; Kroening, Daniel (2017-10-13). "Program
    synthesis: challenges and opportunities". Philosophical
    Transactions of the Royal Society A: Mathematical, Physical and
    Engineering Sciences. 375 (2104): 20150403. doi:10.1098/
    rsta.2015.0403. ISSN 1364-503X. PMC 5597726. PMID 28871052.
 8. ^ SyGuS-Comp (Syntax-Guided Synthesis Competition)
 9. ^ Zohar Manna, Richard Waldinger (Jan 1980). "A Deductive
    Approach to Program Synthesis". ACM Transactions on Programming
    Languages and Systems. 2: 90-121. doi:10.1145/357084.357090.
    S2CID 14770735.
10. ^ Zohar Manna and Richard Waldinger (Dec 1978). A Deductive
    Approach to Program Synthesis (PDF) (Technical Note). SRI
    International. Archived (PDF) from the original on January 27,
    2021.
11. ^ See Manna, Waldinger (1980), p.100 for correctness of the
    resolution rules.
12. ^ Boyer, Robert S.; Moore, J. Strother (May 1983). A Mechanical
    Proof of the Turing Completeness of Pure Lisp (PDF) (Technical
    report). Institute for Computing Science, University of Texas at
    Austin. 37. Archived (PDF) from the original on 22 September
    2017.
13. ^ Manna, Waldinger (1980), p.108-111
14. ^ Zohar Manna and Richard Waldinger (Aug 1987). "The Origin of a
    Binary-Search Paradigm". Science of Computer Programming. 9 (1):
    37-83. doi:10.1016/0167-6423(87)90025-6.
15. ^ Daniele Nardi (1989). "Formal Synthesis of a Unification
    Algorithm by the Deductive-Tableau Method". Journal of Logic
    Programming. 7: 1-43. doi:10.1016/0743-1066(89)90008-3.
16. ^ Daniele Nardi and Riccardo Rosati (1992). "Deductive Synthesis
    of Programs for Query Answering". In Kung-Kiu Lau and Tim Clement
    (ed.). International Workshop on Logic Program Synthesis and
    Transformation (LOPSTR). Workshops in Computing. Springer.
    pp. 15-29. doi:10.1007/978-1-4471-3560-9_2.
17. ^ Jonathan Traugott (1986). "Deductive Synthesis of Sorting
    Programs". Proceedings of the International Conference on
    Automated Deduction. LNCS. Vol. 230. Springer. pp. 641-660.
18. ^ Jonathan Traugott (Jun 1989). "Deductive Synthesis of Sorting
    Programs". Journal of Symbolic Computation. 7 (6): 533-572. doi:
    10.1016/S0747-7171(89)80040-9.
19. ^ Manna, Waldinger (1980), p.99
20. ^ Manna, Waldinger (1980), p.104
21. ^ Manna, Waldinger (1980), p.103, referring to: Neil V. Murray
    (Feb 1979). A Proof Procedure for Quantifier-Free Non-Clausal
    First Order Logic (Technical report). Syracuse Univ. 2-79.
22. ^ Zohar Manna, Richard Waldinger (Jan 1986). "Special Relations
    in Automated Deduction". Journal of the ACM. 33: 1-59. doi:
    10.1145/4904.4905. S2CID 15140138.
23. ^ Zohar Manna, Richard Waldinger (1992). "The Special-Relations
    Rules are Incomplete". Proc. CADE 11. LNCS. Vol. 607. Springer.
    pp. 492-506.

  * Alur, Rajeev; Singh, Rishabh; Fisman, Dana; Solar-Lezama, Armando
    (2018-11-20). "Search-based program synthesis". Communications of
    the ACM. 61 (12): 84-93. doi:10.1145/3208071. ISSN 0001-0782.
  * Zohar Manna, Richard Waldinger (1975). "Knowledge and Reasoning
    in Program Synthesis". Artificial Intelligence. 6 (2): 175-208.
    doi:10.1016/0004-3702(75)90008-9.

*
Retrieved from "https://en.wikipedia.org/w/index.php?title=
Program_synthesis&oldid=1185150452"
Category:

  * Programming paradigms

Hidden categories:

  * Harv and Sfn no-target errors
  * All articles with unsourced statements
  * Articles with unsourced statements from June 2010
  * Articles to be expanded from December 2022
  * All articles to be expanded
  * Articles using small message boxes
  * Articles with unsourced statements from May 2016

  * This page was last edited on 14 November 2023, at 22:02 (UTC).
  * Text is available under the Creative Commons
    Attribution-ShareAlike License 4.0 ; additional terms may apply.
    By using this site, you agree to the Terms of Use and Privacy
    Policy. Wikipedia(r) is a registered trademark of the Wikimedia
    Foundation, Inc., a non-profit organization.

  * Privacy policy
  * About Wikipedia
  * Disclaimers
  * Contact Wikipedia
  * Code of Conduct
  * Developers
  * Statistics
  * Cookie statement
  * Mobile view

  * Wikimedia Foundation
  * Powered by MediaWiki

  * Toggle limited content width