|
Hi HN: Program synthesis generates code from specifications such as test-cases, I-O examples, and assertions. On September 19-20, synthesis researchers will speak about recent breakthroughs and practical tools, aiming the talks at software engineers. We want to extend an invitation to the HN community because the periodic posts on program synthesis and Z3 show interest in the technology. Speakers will include researchers from Stanford, Berkeley, UW, MIT, and Google Brain. Topics will include hw-exploit synthesis, end-user web programming, verification and synthesis of OS level code. 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 of the conference will explain why synthesis reduces to solving an \exists\forall logical 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. |