Speakers include researchers from Stanford, Berkeley, UW, MIT, and Google Brain. As a preview, here are 3 topics that will be covered: hw-exploit synthesis (https://www.cs.princeton.edu/~ctrippel/#publications), end-user web programming (https://schasins.com/papers/), verification and synthesis of OS level code (https://unsat.cs.washington.edu/projects/).

Technical abstracts and registration is on: https://synthetic-minds.com/pages/conference/2019/#program. After the conference we’ll post the slides of the talks.

The foundations part will explain why synthesis reduces to solving an \exists\forall query. More specifically, the query asks “does there exists a program P such that for all inputs x, P(x) computes the correct output?” A solution to the query is the synthesized program P. How to solve the query? The Z3 prover works well for boolean satisfiability (i.e., one \exists query). To solve an \exists\forall query, one approach is to have a two Z3 solvers communicate: one solver synthesizes a candidate program P’ that is correct on a sample of inputs, while the other verifies that P’ is correct on all inputs. If P’s is incorrect, a counterexample input is added to the sample on inputs. The two solvers iterate until the latter is satisfied with the correctness. This process is not unlike GANs; it is called CEGIS (counterexample-guided inductive synthesis) and was invented 2005, and built on an earlier CEGAR (counterexample-guided abstraction refinement) technique from the 90s.

Please comment; or email us with questions.